(0) Obligation:

Clauses:

parse(Xs, T) :- ','(app(As, cons(a, cons(s(A, B, C), cons(b, Bs))), Xs), ','(app(As, cons(s(a, s(A, B, C), b), Bs), Ys), parse(Ys, T))).
parse(Xs, T) :- ','(app(As, cons(a, cons(s(A, B), cons(b, Bs))), Xs), ','(app(As, cons(s(a, s(A, B), b), Bs), Ys), parse(Ys, T))).
parse(Xs, T) :- ','(app(As, cons(a, cons(b, Bs)), Xs), ','(app(As, cons(s(a, b), Bs), Ys), parse(Ys, T))).
parse(cons(s(A, B), nil), s(A, B)).
parse(cons(s(A, B, C), nil), s(A, B, C)).
app(nil, X, X).
app(cons(X, Xs), Ys, cons(X, Zs)) :- app(Xs, Ys, Zs).

Query: parse(g,a)

(1) PrologToDTProblemTransformerProof (SOUND transformation)

Built DT problem from termination graph DT10.

(2) Obligation:

Triples:

appC(cons(X1, X2), X3, X4, X5, X6, cons(X1, X7)) :- appC(X2, X3, X4, X5, X6, X7).
appI(cons(X1, X2), X3, X4, X5, X6, cons(X1, X7)) :- appI(X2, X3, X4, X5, X6, X7).
appE(cons(X1, X2), X3, X4, X5, cons(X1, X6)) :- appE(X2, X3, X4, X5, X6).
appF(cons(X1, X2), X3, X4, X5, cons(X1, X6)) :- appF(X2, X3, X4, X5, X6).
appG(cons(X1, X2), X3, cons(X1, X4)) :- appG(X2, X3, X4).
appH(cons(X1, X2), X3, cons(X1, X4)) :- appH(X2, X3, X4).
parseA(cons(a, cons(s(X1, X2, X3), cons(b, X4))), X5) :- ','(appcB(X1, X2, X3, X4, X6), parseA(X6, X5)).
parseA(cons(X1, X2), X3) :- appC(X4, X5, X6, X7, X8, X2).
parseA(cons(X1, X2), X3) :- ','(appcC(X4, X5, X6, X7, X8, X2), appI(X4, X5, X6, X7, X8, X9)).
parseA(cons(X1, X2), X3) :- ','(appcC(X4, X5, X6, X7, X8, X2), ','(appcD(X1, X4, X5, X6, X7, X8, X9), parseA(X9, X3))).
parseA(X1, X2) :- appE(X3, X4, X5, X6, X1).
parseA(X1, X2) :- ','(appcE(X3, X4, X5, X6, X1), appF(X3, X4, X5, X6, X7)).
parseA(X1, X2) :- ','(appcE(X3, X4, X5, X6, X1), ','(appcF(X3, X4, X5, X6, X7), parseA(X7, X2))).
parseA(X1, X2) :- appG(X3, X4, X1).
parseA(X1, X2) :- ','(appcG(X3, X4, X1), appH(X3, X4, X5)).
parseA(X1, X2) :- ','(appcG(X3, X4, X1), ','(appcH(X3, X4, X5), parseA(X5, X2))).

Clauses:

parsecA(cons(a, cons(s(X1, X2, X3), cons(b, X4))), X5) :- ','(appcB(X1, X2, X3, X4, X6), parsecA(X6, X5)).
parsecA(cons(X1, X2), X3) :- ','(appcC(X4, X5, X6, X7, X8, X2), ','(appcD(X1, X4, X5, X6, X7, X8, X9), parsecA(X9, X3))).
parsecA(X1, X2) :- ','(appcE(X3, X4, X5, X6, X1), ','(appcF(X3, X4, X5, X6, X7), parsecA(X7, X2))).
parsecA(X1, X2) :- ','(appcG(X3, X4, X1), ','(appcH(X3, X4, X5), parsecA(X5, X2))).
parsecA(cons(s(X1, X2), nil), s(X1, X2)).
parsecA(cons(s(X1, X2, X3), nil), s(X1, X2, X3)).
appcC(nil, X1, X2, X3, X4, cons(a, cons(s(X1, X2, X3), cons(b, X4)))).
appcC(cons(X1, X2), X3, X4, X5, X6, cons(X1, X7)) :- appcC(X2, X3, X4, X5, X6, X7).
appcI(nil, X1, X2, X3, X4, cons(s(a, s(X1, X2, X3), b), X4)).
appcI(cons(X1, X2), X3, X4, X5, X6, cons(X1, X7)) :- appcI(X2, X3, X4, X5, X6, X7).
appcE(nil, X1, X2, X3, cons(a, cons(s(X1, X2), cons(b, X3)))).
appcE(cons(X1, X2), X3, X4, X5, cons(X1, X6)) :- appcE(X2, X3, X4, X5, X6).
appcF(nil, X1, X2, X3, cons(s(a, s(X1, X2), b), X3)).
appcF(cons(X1, X2), X3, X4, X5, cons(X1, X6)) :- appcF(X2, X3, X4, X5, X6).
appcG(nil, X1, cons(a, cons(b, X1))).
appcG(cons(X1, X2), X3, cons(X1, X4)) :- appcG(X2, X3, X4).
appcH(nil, X1, cons(s(a, b), X1)).
appcH(cons(X1, X2), X3, cons(X1, X4)) :- appcH(X2, X3, X4).
appcB(X1, X2, X3, X4, cons(s(a, s(X1, X2, X3), b), X4)).
appcD(X1, X2, X3, X4, X5, X6, cons(X1, X7)) :- appcI(X2, X3, X4, X5, X6, X7).

Afs:

parseA(x1, x2)  =  parseA(x1)

(3) TriplesToPiDPProof (SOUND transformation)

We use the technique of [DT09]. With regard to the inferred argument filtering the predicates were used in the following modes:
parseA_in: (b,f)
appC_in: (f,f,f,f,f,b)
appcC_in: (f,f,f,f,f,b)
appI_in: (b,b,b,b,b,f)
appcD_in: (b,b,b,b,b,b,f)
appcI_in: (b,b,b,b,b,f)
appE_in: (f,f,f,f,b)
appcE_in: (f,f,f,f,b)
appF_in: (b,b,b,b,f)
appcF_in: (b,b,b,b,f)
appG_in: (f,f,b)
appcG_in: (f,f,b)
appH_in: (b,b,f)
appcH_in: (b,b,f)
Transforming TRIPLES into the following Term Rewriting System:
Pi DP problem:
The TRS P consists of the following rules:

PARSEA_IN_GA(cons(a, cons(s(X1, X2, X3), cons(b, X4))), X5) → U7_GA(X1, X2, X3, X4, X5, appcB_in_gggga(X1, X2, X3, X4, X6))
U7_GA(X1, X2, X3, X4, X5, appcB_out_gggga(X1, X2, X3, X4, X6)) → U8_GA(X1, X2, X3, X4, X5, parseA_in_ga(X6, X5))
U7_GA(X1, X2, X3, X4, X5, appcB_out_gggga(X1, X2, X3, X4, X6)) → PARSEA_IN_GA(X6, X5)
PARSEA_IN_GA(cons(X1, X2), X3) → U9_GA(X1, X2, X3, appC_in_aaaaag(X4, X5, X6, X7, X8, X2))
PARSEA_IN_GA(cons(X1, X2), X3) → APPC_IN_AAAAAG(X4, X5, X6, X7, X8, X2)
APPC_IN_AAAAAG(cons(X1, X2), X3, X4, X5, X6, cons(X1, X7)) → U1_AAAAAG(X1, X2, X3, X4, X5, X6, X7, appC_in_aaaaag(X2, X3, X4, X5, X6, X7))
APPC_IN_AAAAAG(cons(X1, X2), X3, X4, X5, X6, cons(X1, X7)) → APPC_IN_AAAAAG(X2, X3, X4, X5, X6, X7)
PARSEA_IN_GA(cons(X1, X2), X3) → U10_GA(X1, X2, X3, appcC_in_aaaaag(X4, X5, X6, X7, X8, X2))
U10_GA(X1, X2, X3, appcC_out_aaaaag(X4, X5, X6, X7, X8, X2)) → U11_GA(X1, X2, X3, appI_in_ggggga(X4, X5, X6, X7, X8, X9))
U10_GA(X1, X2, X3, appcC_out_aaaaag(X4, X5, X6, X7, X8, X2)) → APPI_IN_GGGGGA(X4, X5, X6, X7, X8, X9)
APPI_IN_GGGGGA(cons(X1, X2), X3, X4, X5, X6, cons(X1, X7)) → U2_GGGGGA(X1, X2, X3, X4, X5, X6, X7, appI_in_ggggga(X2, X3, X4, X5, X6, X7))
APPI_IN_GGGGGA(cons(X1, X2), X3, X4, X5, X6, cons(X1, X7)) → APPI_IN_GGGGGA(X2, X3, X4, X5, X6, X7)
U10_GA(X1, X2, X3, appcC_out_aaaaag(X4, X5, X6, X7, X8, X2)) → U12_GA(X1, X2, X3, appcD_in_gggggga(X1, X4, X5, X6, X7, X8, X9))
U12_GA(X1, X2, X3, appcD_out_gggggga(X1, X4, X5, X6, X7, X8, X9)) → U13_GA(X1, X2, X3, parseA_in_ga(X9, X3))
U12_GA(X1, X2, X3, appcD_out_gggggga(X1, X4, X5, X6, X7, X8, X9)) → PARSEA_IN_GA(X9, X3)
PARSEA_IN_GA(X1, X2) → U14_GA(X1, X2, appE_in_aaaag(X3, X4, X5, X6, X1))
PARSEA_IN_GA(X1, X2) → APPE_IN_AAAAG(X3, X4, X5, X6, X1)
APPE_IN_AAAAG(cons(X1, X2), X3, X4, X5, cons(X1, X6)) → U3_AAAAG(X1, X2, X3, X4, X5, X6, appE_in_aaaag(X2, X3, X4, X5, X6))
APPE_IN_AAAAG(cons(X1, X2), X3, X4, X5, cons(X1, X6)) → APPE_IN_AAAAG(X2, X3, X4, X5, X6)
PARSEA_IN_GA(X1, X2) → U15_GA(X1, X2, appcE_in_aaaag(X3, X4, X5, X6, X1))
U15_GA(X1, X2, appcE_out_aaaag(X3, X4, X5, X6, X1)) → U16_GA(X1, X2, appF_in_gggga(X3, X4, X5, X6, X7))
U15_GA(X1, X2, appcE_out_aaaag(X3, X4, X5, X6, X1)) → APPF_IN_GGGGA(X3, X4, X5, X6, X7)
APPF_IN_GGGGA(cons(X1, X2), X3, X4, X5, cons(X1, X6)) → U4_GGGGA(X1, X2, X3, X4, X5, X6, appF_in_gggga(X2, X3, X4, X5, X6))
APPF_IN_GGGGA(cons(X1, X2), X3, X4, X5, cons(X1, X6)) → APPF_IN_GGGGA(X2, X3, X4, X5, X6)
U15_GA(X1, X2, appcE_out_aaaag(X3, X4, X5, X6, X1)) → U17_GA(X1, X2, appcF_in_gggga(X3, X4, X5, X6, X7))
U17_GA(X1, X2, appcF_out_gggga(X3, X4, X5, X6, X7)) → U18_GA(X1, X2, parseA_in_ga(X7, X2))
U17_GA(X1, X2, appcF_out_gggga(X3, X4, X5, X6, X7)) → PARSEA_IN_GA(X7, X2)
PARSEA_IN_GA(X1, X2) → U19_GA(X1, X2, appG_in_aag(X3, X4, X1))
PARSEA_IN_GA(X1, X2) → APPG_IN_AAG(X3, X4, X1)
APPG_IN_AAG(cons(X1, X2), X3, cons(X1, X4)) → U5_AAG(X1, X2, X3, X4, appG_in_aag(X2, X3, X4))
APPG_IN_AAG(cons(X1, X2), X3, cons(X1, X4)) → APPG_IN_AAG(X2, X3, X4)
PARSEA_IN_GA(X1, X2) → U20_GA(X1, X2, appcG_in_aag(X3, X4, X1))
U20_GA(X1, X2, appcG_out_aag(X3, X4, X1)) → U21_GA(X1, X2, appH_in_gga(X3, X4, X5))
U20_GA(X1, X2, appcG_out_aag(X3, X4, X1)) → APPH_IN_GGA(X3, X4, X5)
APPH_IN_GGA(cons(X1, X2), X3, cons(X1, X4)) → U6_GGA(X1, X2, X3, X4, appH_in_gga(X2, X3, X4))
APPH_IN_GGA(cons(X1, X2), X3, cons(X1, X4)) → APPH_IN_GGA(X2, X3, X4)
U20_GA(X1, X2, appcG_out_aag(X3, X4, X1)) → U22_GA(X1, X2, appcH_in_gga(X3, X4, X5))
U22_GA(X1, X2, appcH_out_gga(X3, X4, X5)) → U23_GA(X1, X2, parseA_in_ga(X5, X2))
U22_GA(X1, X2, appcH_out_gga(X3, X4, X5)) → PARSEA_IN_GA(X5, X2)

The TRS R consists of the following rules:

appcB_in_gggga(X1, X2, X3, X4, cons(s(a, s(X1, X2, X3), b), X4)) → appcB_out_gggga(X1, X2, X3, X4, cons(s(a, s(X1, X2, X3), b), X4))
appcC_in_aaaaag(nil, X1, X2, X3, X4, cons(a, cons(s(X1, X2, X3), cons(b, X4)))) → appcC_out_aaaaag(nil, X1, X2, X3, X4, cons(a, cons(s(X1, X2, X3), cons(b, X4))))
appcC_in_aaaaag(cons(X1, X2), X3, X4, X5, X6, cons(X1, X7)) → U36_aaaaag(X1, X2, X3, X4, X5, X6, X7, appcC_in_aaaaag(X2, X3, X4, X5, X6, X7))
U36_aaaaag(X1, X2, X3, X4, X5, X6, X7, appcC_out_aaaaag(X2, X3, X4, X5, X6, X7)) → appcC_out_aaaaag(cons(X1, X2), X3, X4, X5, X6, cons(X1, X7))
appcD_in_gggggga(X1, X2, X3, X4, X5, X6, cons(X1, X7)) → U42_gggggga(X1, X2, X3, X4, X5, X6, X7, appcI_in_ggggga(X2, X3, X4, X5, X6, X7))
appcI_in_ggggga(nil, X1, X2, X3, X4, cons(s(a, s(X1, X2, X3), b), X4)) → appcI_out_ggggga(nil, X1, X2, X3, X4, cons(s(a, s(X1, X2, X3), b), X4))
appcI_in_ggggga(cons(X1, X2), X3, X4, X5, X6, cons(X1, X7)) → U37_ggggga(X1, X2, X3, X4, X5, X6, X7, appcI_in_ggggga(X2, X3, X4, X5, X6, X7))
U37_ggggga(X1, X2, X3, X4, X5, X6, X7, appcI_out_ggggga(X2, X3, X4, X5, X6, X7)) → appcI_out_ggggga(cons(X1, X2), X3, X4, X5, X6, cons(X1, X7))
U42_gggggga(X1, X2, X3, X4, X5, X6, X7, appcI_out_ggggga(X2, X3, X4, X5, X6, X7)) → appcD_out_gggggga(X1, X2, X3, X4, X5, X6, cons(X1, X7))
appcE_in_aaaag(nil, X1, X2, X3, cons(a, cons(s(X1, X2), cons(b, X3)))) → appcE_out_aaaag(nil, X1, X2, X3, cons(a, cons(s(X1, X2), cons(b, X3))))
appcE_in_aaaag(cons(X1, X2), X3, X4, X5, cons(X1, X6)) → U38_aaaag(X1, X2, X3, X4, X5, X6, appcE_in_aaaag(X2, X3, X4, X5, X6))
U38_aaaag(X1, X2, X3, X4, X5, X6, appcE_out_aaaag(X2, X3, X4, X5, X6)) → appcE_out_aaaag(cons(X1, X2), X3, X4, X5, cons(X1, X6))
appcF_in_gggga(nil, X1, X2, X3, cons(s(a, s(X1, X2), b), X3)) → appcF_out_gggga(nil, X1, X2, X3, cons(s(a, s(X1, X2), b), X3))
appcF_in_gggga(cons(X1, X2), X3, X4, X5, cons(X1, X6)) → U39_gggga(X1, X2, X3, X4, X5, X6, appcF_in_gggga(X2, X3, X4, X5, X6))
U39_gggga(X1, X2, X3, X4, X5, X6, appcF_out_gggga(X2, X3, X4, X5, X6)) → appcF_out_gggga(cons(X1, X2), X3, X4, X5, cons(X1, X6))
appcG_in_aag(nil, X1, cons(a, cons(b, X1))) → appcG_out_aag(nil, X1, cons(a, cons(b, X1)))
appcG_in_aag(cons(X1, X2), X3, cons(X1, X4)) → U40_aag(X1, X2, X3, X4, appcG_in_aag(X2, X3, X4))
U40_aag(X1, X2, X3, X4, appcG_out_aag(X2, X3, X4)) → appcG_out_aag(cons(X1, X2), X3, cons(X1, X4))
appcH_in_gga(nil, X1, cons(s(a, b), X1)) → appcH_out_gga(nil, X1, cons(s(a, b), X1))
appcH_in_gga(cons(X1, X2), X3, cons(X1, X4)) → U41_gga(X1, X2, X3, X4, appcH_in_gga(X2, X3, X4))
U41_gga(X1, X2, X3, X4, appcH_out_gga(X2, X3, X4)) → appcH_out_gga(cons(X1, X2), X3, cons(X1, X4))

The argument filtering Pi contains the following mapping:
parseA_in_ga(x1, x2)  =  parseA_in_ga(x1)
cons(x1, x2)  =  cons(x1, x2)
a  =  a
s(x1, x2, x3)  =  s(x1, x2, x3)
b  =  b
appcB_in_gggga(x1, x2, x3, x4, x5)  =  appcB_in_gggga(x1, x2, x3, x4)
appcB_out_gggga(x1, x2, x3, x4, x5)  =  appcB_out_gggga(x1, x2, x3, x4, x5)
appC_in_aaaaag(x1, x2, x3, x4, x5, x6)  =  appC_in_aaaaag(x6)
appcC_in_aaaaag(x1, x2, x3, x4, x5, x6)  =  appcC_in_aaaaag(x6)
appcC_out_aaaaag(x1, x2, x3, x4, x5, x6)  =  appcC_out_aaaaag(x1, x2, x3, x4, x5, x6)
U36_aaaaag(x1, x2, x3, x4, x5, x6, x7, x8)  =  U36_aaaaag(x1, x7, x8)
appI_in_ggggga(x1, x2, x3, x4, x5, x6)  =  appI_in_ggggga(x1, x2, x3, x4, x5)
appcD_in_gggggga(x1, x2, x3, x4, x5, x6, x7)  =  appcD_in_gggggga(x1, x2, x3, x4, x5, x6)
U42_gggggga(x1, x2, x3, x4, x5, x6, x7, x8)  =  U42_gggggga(x1, x2, x3, x4, x5, x6, x8)
appcI_in_ggggga(x1, x2, x3, x4, x5, x6)  =  appcI_in_ggggga(x1, x2, x3, x4, x5)
nil  =  nil
appcI_out_ggggga(x1, x2, x3, x4, x5, x6)  =  appcI_out_ggggga(x1, x2, x3, x4, x5, x6)
U37_ggggga(x1, x2, x3, x4, x5, x6, x7, x8)  =  U37_ggggga(x1, x2, x3, x4, x5, x6, x8)
appcD_out_gggggga(x1, x2, x3, x4, x5, x6, x7)  =  appcD_out_gggggga(x1, x2, x3, x4, x5, x6, x7)
appE_in_aaaag(x1, x2, x3, x4, x5)  =  appE_in_aaaag(x5)
appcE_in_aaaag(x1, x2, x3, x4, x5)  =  appcE_in_aaaag(x5)
s(x1, x2)  =  s(x1, x2)
appcE_out_aaaag(x1, x2, x3, x4, x5)  =  appcE_out_aaaag(x1, x2, x3, x4, x5)
U38_aaaag(x1, x2, x3, x4, x5, x6, x7)  =  U38_aaaag(x1, x6, x7)
appF_in_gggga(x1, x2, x3, x4, x5)  =  appF_in_gggga(x1, x2, x3, x4)
appcF_in_gggga(x1, x2, x3, x4, x5)  =  appcF_in_gggga(x1, x2, x3, x4)
appcF_out_gggga(x1, x2, x3, x4, x5)  =  appcF_out_gggga(x1, x2, x3, x4, x5)
U39_gggga(x1, x2, x3, x4, x5, x6, x7)  =  U39_gggga(x1, x2, x3, x4, x5, x7)
appG_in_aag(x1, x2, x3)  =  appG_in_aag(x3)
appcG_in_aag(x1, x2, x3)  =  appcG_in_aag(x3)
appcG_out_aag(x1, x2, x3)  =  appcG_out_aag(x1, x2, x3)
U40_aag(x1, x2, x3, x4, x5)  =  U40_aag(x1, x4, x5)
appH_in_gga(x1, x2, x3)  =  appH_in_gga(x1, x2)
appcH_in_gga(x1, x2, x3)  =  appcH_in_gga(x1, x2)
appcH_out_gga(x1, x2, x3)  =  appcH_out_gga(x1, x2, x3)
U41_gga(x1, x2, x3, x4, x5)  =  U41_gga(x1, x2, x3, x5)
PARSEA_IN_GA(x1, x2)  =  PARSEA_IN_GA(x1)
U7_GA(x1, x2, x3, x4, x5, x6)  =  U7_GA(x1, x2, x3, x4, x6)
U8_GA(x1, x2, x3, x4, x5, x6)  =  U8_GA(x1, x2, x3, x4, x6)
U9_GA(x1, x2, x3, x4)  =  U9_GA(x1, x2, x4)
APPC_IN_AAAAAG(x1, x2, x3, x4, x5, x6)  =  APPC_IN_AAAAAG(x6)
U1_AAAAAG(x1, x2, x3, x4, x5, x6, x7, x8)  =  U1_AAAAAG(x1, x7, x8)
U10_GA(x1, x2, x3, x4)  =  U10_GA(x1, x2, x4)
U11_GA(x1, x2, x3, x4)  =  U11_GA(x1, x2, x4)
APPI_IN_GGGGGA(x1, x2, x3, x4, x5, x6)  =  APPI_IN_GGGGGA(x1, x2, x3, x4, x5)
U2_GGGGGA(x1, x2, x3, x4, x5, x6, x7, x8)  =  U2_GGGGGA(x1, x2, x3, x4, x5, x6, x8)
U12_GA(x1, x2, x3, x4)  =  U12_GA(x1, x2, x4)
U13_GA(x1, x2, x3, x4)  =  U13_GA(x1, x2, x4)
U14_GA(x1, x2, x3)  =  U14_GA(x1, x3)
APPE_IN_AAAAG(x1, x2, x3, x4, x5)  =  APPE_IN_AAAAG(x5)
U3_AAAAG(x1, x2, x3, x4, x5, x6, x7)  =  U3_AAAAG(x1, x6, x7)
U15_GA(x1, x2, x3)  =  U15_GA(x1, x3)
U16_GA(x1, x2, x3)  =  U16_GA(x1, x3)
APPF_IN_GGGGA(x1, x2, x3, x4, x5)  =  APPF_IN_GGGGA(x1, x2, x3, x4)
U4_GGGGA(x1, x2, x3, x4, x5, x6, x7)  =  U4_GGGGA(x1, x2, x3, x4, x5, x7)
U17_GA(x1, x2, x3)  =  U17_GA(x1, x3)
U18_GA(x1, x2, x3)  =  U18_GA(x1, x3)
U19_GA(x1, x2, x3)  =  U19_GA(x1, x3)
APPG_IN_AAG(x1, x2, x3)  =  APPG_IN_AAG(x3)
U5_AAG(x1, x2, x3, x4, x5)  =  U5_AAG(x1, x4, x5)
U20_GA(x1, x2, x3)  =  U20_GA(x1, x3)
U21_GA(x1, x2, x3)  =  U21_GA(x1, x3)
APPH_IN_GGA(x1, x2, x3)  =  APPH_IN_GGA(x1, x2)
U6_GGA(x1, x2, x3, x4, x5)  =  U6_GGA(x1, x2, x3, x5)
U22_GA(x1, x2, x3)  =  U22_GA(x1, x3)
U23_GA(x1, x2, x3)  =  U23_GA(x1, x3)

We have to consider all (P,R,Pi)-chains

Infinitary Constructor Rewriting Termination of PiDP implies Termination of TRIPLES

(4) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

PARSEA_IN_GA(cons(a, cons(s(X1, X2, X3), cons(b, X4))), X5) → U7_GA(X1, X2, X3, X4, X5, appcB_in_gggga(X1, X2, X3, X4, X6))
U7_GA(X1, X2, X3, X4, X5, appcB_out_gggga(X1, X2, X3, X4, X6)) → U8_GA(X1, X2, X3, X4, X5, parseA_in_ga(X6, X5))
U7_GA(X1, X2, X3, X4, X5, appcB_out_gggga(X1, X2, X3, X4, X6)) → PARSEA_IN_GA(X6, X5)
PARSEA_IN_GA(cons(X1, X2), X3) → U9_GA(X1, X2, X3, appC_in_aaaaag(X4, X5, X6, X7, X8, X2))
PARSEA_IN_GA(cons(X1, X2), X3) → APPC_IN_AAAAAG(X4, X5, X6, X7, X8, X2)
APPC_IN_AAAAAG(cons(X1, X2), X3, X4, X5, X6, cons(X1, X7)) → U1_AAAAAG(X1, X2, X3, X4, X5, X6, X7, appC_in_aaaaag(X2, X3, X4, X5, X6, X7))
APPC_IN_AAAAAG(cons(X1, X2), X3, X4, X5, X6, cons(X1, X7)) → APPC_IN_AAAAAG(X2, X3, X4, X5, X6, X7)
PARSEA_IN_GA(cons(X1, X2), X3) → U10_GA(X1, X2, X3, appcC_in_aaaaag(X4, X5, X6, X7, X8, X2))
U10_GA(X1, X2, X3, appcC_out_aaaaag(X4, X5, X6, X7, X8, X2)) → U11_GA(X1, X2, X3, appI_in_ggggga(X4, X5, X6, X7, X8, X9))
U10_GA(X1, X2, X3, appcC_out_aaaaag(X4, X5, X6, X7, X8, X2)) → APPI_IN_GGGGGA(X4, X5, X6, X7, X8, X9)
APPI_IN_GGGGGA(cons(X1, X2), X3, X4, X5, X6, cons(X1, X7)) → U2_GGGGGA(X1, X2, X3, X4, X5, X6, X7, appI_in_ggggga(X2, X3, X4, X5, X6, X7))
APPI_IN_GGGGGA(cons(X1, X2), X3, X4, X5, X6, cons(X1, X7)) → APPI_IN_GGGGGA(X2, X3, X4, X5, X6, X7)
U10_GA(X1, X2, X3, appcC_out_aaaaag(X4, X5, X6, X7, X8, X2)) → U12_GA(X1, X2, X3, appcD_in_gggggga(X1, X4, X5, X6, X7, X8, X9))
U12_GA(X1, X2, X3, appcD_out_gggggga(X1, X4, X5, X6, X7, X8, X9)) → U13_GA(X1, X2, X3, parseA_in_ga(X9, X3))
U12_GA(X1, X2, X3, appcD_out_gggggga(X1, X4, X5, X6, X7, X8, X9)) → PARSEA_IN_GA(X9, X3)
PARSEA_IN_GA(X1, X2) → U14_GA(X1, X2, appE_in_aaaag(X3, X4, X5, X6, X1))
PARSEA_IN_GA(X1, X2) → APPE_IN_AAAAG(X3, X4, X5, X6, X1)
APPE_IN_AAAAG(cons(X1, X2), X3, X4, X5, cons(X1, X6)) → U3_AAAAG(X1, X2, X3, X4, X5, X6, appE_in_aaaag(X2, X3, X4, X5, X6))
APPE_IN_AAAAG(cons(X1, X2), X3, X4, X5, cons(X1, X6)) → APPE_IN_AAAAG(X2, X3, X4, X5, X6)
PARSEA_IN_GA(X1, X2) → U15_GA(X1, X2, appcE_in_aaaag(X3, X4, X5, X6, X1))
U15_GA(X1, X2, appcE_out_aaaag(X3, X4, X5, X6, X1)) → U16_GA(X1, X2, appF_in_gggga(X3, X4, X5, X6, X7))
U15_GA(X1, X2, appcE_out_aaaag(X3, X4, X5, X6, X1)) → APPF_IN_GGGGA(X3, X4, X5, X6, X7)
APPF_IN_GGGGA(cons(X1, X2), X3, X4, X5, cons(X1, X6)) → U4_GGGGA(X1, X2, X3, X4, X5, X6, appF_in_gggga(X2, X3, X4, X5, X6))
APPF_IN_GGGGA(cons(X1, X2), X3, X4, X5, cons(X1, X6)) → APPF_IN_GGGGA(X2, X3, X4, X5, X6)
U15_GA(X1, X2, appcE_out_aaaag(X3, X4, X5, X6, X1)) → U17_GA(X1, X2, appcF_in_gggga(X3, X4, X5, X6, X7))
U17_GA(X1, X2, appcF_out_gggga(X3, X4, X5, X6, X7)) → U18_GA(X1, X2, parseA_in_ga(X7, X2))
U17_GA(X1, X2, appcF_out_gggga(X3, X4, X5, X6, X7)) → PARSEA_IN_GA(X7, X2)
PARSEA_IN_GA(X1, X2) → U19_GA(X1, X2, appG_in_aag(X3, X4, X1))
PARSEA_IN_GA(X1, X2) → APPG_IN_AAG(X3, X4, X1)
APPG_IN_AAG(cons(X1, X2), X3, cons(X1, X4)) → U5_AAG(X1, X2, X3, X4, appG_in_aag(X2, X3, X4))
APPG_IN_AAG(cons(X1, X2), X3, cons(X1, X4)) → APPG_IN_AAG(X2, X3, X4)
PARSEA_IN_GA(X1, X2) → U20_GA(X1, X2, appcG_in_aag(X3, X4, X1))
U20_GA(X1, X2, appcG_out_aag(X3, X4, X1)) → U21_GA(X1, X2, appH_in_gga(X3, X4, X5))
U20_GA(X1, X2, appcG_out_aag(X3, X4, X1)) → APPH_IN_GGA(X3, X4, X5)
APPH_IN_GGA(cons(X1, X2), X3, cons(X1, X4)) → U6_GGA(X1, X2, X3, X4, appH_in_gga(X2, X3, X4))
APPH_IN_GGA(cons(X1, X2), X3, cons(X1, X4)) → APPH_IN_GGA(X2, X3, X4)
U20_GA(X1, X2, appcG_out_aag(X3, X4, X1)) → U22_GA(X1, X2, appcH_in_gga(X3, X4, X5))
U22_GA(X1, X2, appcH_out_gga(X3, X4, X5)) → U23_GA(X1, X2, parseA_in_ga(X5, X2))
U22_GA(X1, X2, appcH_out_gga(X3, X4, X5)) → PARSEA_IN_GA(X5, X2)

The TRS R consists of the following rules:

appcB_in_gggga(X1, X2, X3, X4, cons(s(a, s(X1, X2, X3), b), X4)) → appcB_out_gggga(X1, X2, X3, X4, cons(s(a, s(X1, X2, X3), b), X4))
appcC_in_aaaaag(nil, X1, X2, X3, X4, cons(a, cons(s(X1, X2, X3), cons(b, X4)))) → appcC_out_aaaaag(nil, X1, X2, X3, X4, cons(a, cons(s(X1, X2, X3), cons(b, X4))))
appcC_in_aaaaag(cons(X1, X2), X3, X4, X5, X6, cons(X1, X7)) → U36_aaaaag(X1, X2, X3, X4, X5, X6, X7, appcC_in_aaaaag(X2, X3, X4, X5, X6, X7))
U36_aaaaag(X1, X2, X3, X4, X5, X6, X7, appcC_out_aaaaag(X2, X3, X4, X5, X6, X7)) → appcC_out_aaaaag(cons(X1, X2), X3, X4, X5, X6, cons(X1, X7))
appcD_in_gggggga(X1, X2, X3, X4, X5, X6, cons(X1, X7)) → U42_gggggga(X1, X2, X3, X4, X5, X6, X7, appcI_in_ggggga(X2, X3, X4, X5, X6, X7))
appcI_in_ggggga(nil, X1, X2, X3, X4, cons(s(a, s(X1, X2, X3), b), X4)) → appcI_out_ggggga(nil, X1, X2, X3, X4, cons(s(a, s(X1, X2, X3), b), X4))
appcI_in_ggggga(cons(X1, X2), X3, X4, X5, X6, cons(X1, X7)) → U37_ggggga(X1, X2, X3, X4, X5, X6, X7, appcI_in_ggggga(X2, X3, X4, X5, X6, X7))
U37_ggggga(X1, X2, X3, X4, X5, X6, X7, appcI_out_ggggga(X2, X3, X4, X5, X6, X7)) → appcI_out_ggggga(cons(X1, X2), X3, X4, X5, X6, cons(X1, X7))
U42_gggggga(X1, X2, X3, X4, X5, X6, X7, appcI_out_ggggga(X2, X3, X4, X5, X6, X7)) → appcD_out_gggggga(X1, X2, X3, X4, X5, X6, cons(X1, X7))
appcE_in_aaaag(nil, X1, X2, X3, cons(a, cons(s(X1, X2), cons(b, X3)))) → appcE_out_aaaag(nil, X1, X2, X3, cons(a, cons(s(X1, X2), cons(b, X3))))
appcE_in_aaaag(cons(X1, X2), X3, X4, X5, cons(X1, X6)) → U38_aaaag(X1, X2, X3, X4, X5, X6, appcE_in_aaaag(X2, X3, X4, X5, X6))
U38_aaaag(X1, X2, X3, X4, X5, X6, appcE_out_aaaag(X2, X3, X4, X5, X6)) → appcE_out_aaaag(cons(X1, X2), X3, X4, X5, cons(X1, X6))
appcF_in_gggga(nil, X1, X2, X3, cons(s(a, s(X1, X2), b), X3)) → appcF_out_gggga(nil, X1, X2, X3, cons(s(a, s(X1, X2), b), X3))
appcF_in_gggga(cons(X1, X2), X3, X4, X5, cons(X1, X6)) → U39_gggga(X1, X2, X3, X4, X5, X6, appcF_in_gggga(X2, X3, X4, X5, X6))
U39_gggga(X1, X2, X3, X4, X5, X6, appcF_out_gggga(X2, X3, X4, X5, X6)) → appcF_out_gggga(cons(X1, X2), X3, X4, X5, cons(X1, X6))
appcG_in_aag(nil, X1, cons(a, cons(b, X1))) → appcG_out_aag(nil, X1, cons(a, cons(b, X1)))
appcG_in_aag(cons(X1, X2), X3, cons(X1, X4)) → U40_aag(X1, X2, X3, X4, appcG_in_aag(X2, X3, X4))
U40_aag(X1, X2, X3, X4, appcG_out_aag(X2, X3, X4)) → appcG_out_aag(cons(X1, X2), X3, cons(X1, X4))
appcH_in_gga(nil, X1, cons(s(a, b), X1)) → appcH_out_gga(nil, X1, cons(s(a, b), X1))
appcH_in_gga(cons(X1, X2), X3, cons(X1, X4)) → U41_gga(X1, X2, X3, X4, appcH_in_gga(X2, X3, X4))
U41_gga(X1, X2, X3, X4, appcH_out_gga(X2, X3, X4)) → appcH_out_gga(cons(X1, X2), X3, cons(X1, X4))

The argument filtering Pi contains the following mapping:
parseA_in_ga(x1, x2)  =  parseA_in_ga(x1)
cons(x1, x2)  =  cons(x1, x2)
a  =  a
s(x1, x2, x3)  =  s(x1, x2, x3)
b  =  b
appcB_in_gggga(x1, x2, x3, x4, x5)  =  appcB_in_gggga(x1, x2, x3, x4)
appcB_out_gggga(x1, x2, x3, x4, x5)  =  appcB_out_gggga(x1, x2, x3, x4, x5)
appC_in_aaaaag(x1, x2, x3, x4, x5, x6)  =  appC_in_aaaaag(x6)
appcC_in_aaaaag(x1, x2, x3, x4, x5, x6)  =  appcC_in_aaaaag(x6)
appcC_out_aaaaag(x1, x2, x3, x4, x5, x6)  =  appcC_out_aaaaag(x1, x2, x3, x4, x5, x6)
U36_aaaaag(x1, x2, x3, x4, x5, x6, x7, x8)  =  U36_aaaaag(x1, x7, x8)
appI_in_ggggga(x1, x2, x3, x4, x5, x6)  =  appI_in_ggggga(x1, x2, x3, x4, x5)
appcD_in_gggggga(x1, x2, x3, x4, x5, x6, x7)  =  appcD_in_gggggga(x1, x2, x3, x4, x5, x6)
U42_gggggga(x1, x2, x3, x4, x5, x6, x7, x8)  =  U42_gggggga(x1, x2, x3, x4, x5, x6, x8)
appcI_in_ggggga(x1, x2, x3, x4, x5, x6)  =  appcI_in_ggggga(x1, x2, x3, x4, x5)
nil  =  nil
appcI_out_ggggga(x1, x2, x3, x4, x5, x6)  =  appcI_out_ggggga(x1, x2, x3, x4, x5, x6)
U37_ggggga(x1, x2, x3, x4, x5, x6, x7, x8)  =  U37_ggggga(x1, x2, x3, x4, x5, x6, x8)
appcD_out_gggggga(x1, x2, x3, x4, x5, x6, x7)  =  appcD_out_gggggga(x1, x2, x3, x4, x5, x6, x7)
appE_in_aaaag(x1, x2, x3, x4, x5)  =  appE_in_aaaag(x5)
appcE_in_aaaag(x1, x2, x3, x4, x5)  =  appcE_in_aaaag(x5)
s(x1, x2)  =  s(x1, x2)
appcE_out_aaaag(x1, x2, x3, x4, x5)  =  appcE_out_aaaag(x1, x2, x3, x4, x5)
U38_aaaag(x1, x2, x3, x4, x5, x6, x7)  =  U38_aaaag(x1, x6, x7)
appF_in_gggga(x1, x2, x3, x4, x5)  =  appF_in_gggga(x1, x2, x3, x4)
appcF_in_gggga(x1, x2, x3, x4, x5)  =  appcF_in_gggga(x1, x2, x3, x4)
appcF_out_gggga(x1, x2, x3, x4, x5)  =  appcF_out_gggga(x1, x2, x3, x4, x5)
U39_gggga(x1, x2, x3, x4, x5, x6, x7)  =  U39_gggga(x1, x2, x3, x4, x5, x7)
appG_in_aag(x1, x2, x3)  =  appG_in_aag(x3)
appcG_in_aag(x1, x2, x3)  =  appcG_in_aag(x3)
appcG_out_aag(x1, x2, x3)  =  appcG_out_aag(x1, x2, x3)
U40_aag(x1, x2, x3, x4, x5)  =  U40_aag(x1, x4, x5)
appH_in_gga(x1, x2, x3)  =  appH_in_gga(x1, x2)
appcH_in_gga(x1, x2, x3)  =  appcH_in_gga(x1, x2)
appcH_out_gga(x1, x2, x3)  =  appcH_out_gga(x1, x2, x3)
U41_gga(x1, x2, x3, x4, x5)  =  U41_gga(x1, x2, x3, x5)
PARSEA_IN_GA(x1, x2)  =  PARSEA_IN_GA(x1)
U7_GA(x1, x2, x3, x4, x5, x6)  =  U7_GA(x1, x2, x3, x4, x6)
U8_GA(x1, x2, x3, x4, x5, x6)  =  U8_GA(x1, x2, x3, x4, x6)
U9_GA(x1, x2, x3, x4)  =  U9_GA(x1, x2, x4)
APPC_IN_AAAAAG(x1, x2, x3, x4, x5, x6)  =  APPC_IN_AAAAAG(x6)
U1_AAAAAG(x1, x2, x3, x4, x5, x6, x7, x8)  =  U1_AAAAAG(x1, x7, x8)
U10_GA(x1, x2, x3, x4)  =  U10_GA(x1, x2, x4)
U11_GA(x1, x2, x3, x4)  =  U11_GA(x1, x2, x4)
APPI_IN_GGGGGA(x1, x2, x3, x4, x5, x6)  =  APPI_IN_GGGGGA(x1, x2, x3, x4, x5)
U2_GGGGGA(x1, x2, x3, x4, x5, x6, x7, x8)  =  U2_GGGGGA(x1, x2, x3, x4, x5, x6, x8)
U12_GA(x1, x2, x3, x4)  =  U12_GA(x1, x2, x4)
U13_GA(x1, x2, x3, x4)  =  U13_GA(x1, x2, x4)
U14_GA(x1, x2, x3)  =  U14_GA(x1, x3)
APPE_IN_AAAAG(x1, x2, x3, x4, x5)  =  APPE_IN_AAAAG(x5)
U3_AAAAG(x1, x2, x3, x4, x5, x6, x7)  =  U3_AAAAG(x1, x6, x7)
U15_GA(x1, x2, x3)  =  U15_GA(x1, x3)
U16_GA(x1, x2, x3)  =  U16_GA(x1, x3)
APPF_IN_GGGGA(x1, x2, x3, x4, x5)  =  APPF_IN_GGGGA(x1, x2, x3, x4)
U4_GGGGA(x1, x2, x3, x4, x5, x6, x7)  =  U4_GGGGA(x1, x2, x3, x4, x5, x7)
U17_GA(x1, x2, x3)  =  U17_GA(x1, x3)
U18_GA(x1, x2, x3)  =  U18_GA(x1, x3)
U19_GA(x1, x2, x3)  =  U19_GA(x1, x3)
APPG_IN_AAG(x1, x2, x3)  =  APPG_IN_AAG(x3)
U5_AAG(x1, x2, x3, x4, x5)  =  U5_AAG(x1, x4, x5)
U20_GA(x1, x2, x3)  =  U20_GA(x1, x3)
U21_GA(x1, x2, x3)  =  U21_GA(x1, x3)
APPH_IN_GGA(x1, x2, x3)  =  APPH_IN_GGA(x1, x2)
U6_GGA(x1, x2, x3, x4, x5)  =  U6_GGA(x1, x2, x3, x5)
U22_GA(x1, x2, x3)  =  U22_GA(x1, x3)
U23_GA(x1, x2, x3)  =  U23_GA(x1, x3)

We have to consider all (P,R,Pi)-chains

(5) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 7 SCCs with 22 less nodes.

(6) Complex Obligation (AND)

(7) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

APPH_IN_GGA(cons(X1, X2), X3, cons(X1, X4)) → APPH_IN_GGA(X2, X3, X4)

The TRS R consists of the following rules:

appcB_in_gggga(X1, X2, X3, X4, cons(s(a, s(X1, X2, X3), b), X4)) → appcB_out_gggga(X1, X2, X3, X4, cons(s(a, s(X1, X2, X3), b), X4))
appcC_in_aaaaag(nil, X1, X2, X3, X4, cons(a, cons(s(X1, X2, X3), cons(b, X4)))) → appcC_out_aaaaag(nil, X1, X2, X3, X4, cons(a, cons(s(X1, X2, X3), cons(b, X4))))
appcC_in_aaaaag(cons(X1, X2), X3, X4, X5, X6, cons(X1, X7)) → U36_aaaaag(X1, X2, X3, X4, X5, X6, X7, appcC_in_aaaaag(X2, X3, X4, X5, X6, X7))
U36_aaaaag(X1, X2, X3, X4, X5, X6, X7, appcC_out_aaaaag(X2, X3, X4, X5, X6, X7)) → appcC_out_aaaaag(cons(X1, X2), X3, X4, X5, X6, cons(X1, X7))
appcD_in_gggggga(X1, X2, X3, X4, X5, X6, cons(X1, X7)) → U42_gggggga(X1, X2, X3, X4, X5, X6, X7, appcI_in_ggggga(X2, X3, X4, X5, X6, X7))
appcI_in_ggggga(nil, X1, X2, X3, X4, cons(s(a, s(X1, X2, X3), b), X4)) → appcI_out_ggggga(nil, X1, X2, X3, X4, cons(s(a, s(X1, X2, X3), b), X4))
appcI_in_ggggga(cons(X1, X2), X3, X4, X5, X6, cons(X1, X7)) → U37_ggggga(X1, X2, X3, X4, X5, X6, X7, appcI_in_ggggga(X2, X3, X4, X5, X6, X7))
U37_ggggga(X1, X2, X3, X4, X5, X6, X7, appcI_out_ggggga(X2, X3, X4, X5, X6, X7)) → appcI_out_ggggga(cons(X1, X2), X3, X4, X5, X6, cons(X1, X7))
U42_gggggga(X1, X2, X3, X4, X5, X6, X7, appcI_out_ggggga(X2, X3, X4, X5, X6, X7)) → appcD_out_gggggga(X1, X2, X3, X4, X5, X6, cons(X1, X7))
appcE_in_aaaag(nil, X1, X2, X3, cons(a, cons(s(X1, X2), cons(b, X3)))) → appcE_out_aaaag(nil, X1, X2, X3, cons(a, cons(s(X1, X2), cons(b, X3))))
appcE_in_aaaag(cons(X1, X2), X3, X4, X5, cons(X1, X6)) → U38_aaaag(X1, X2, X3, X4, X5, X6, appcE_in_aaaag(X2, X3, X4, X5, X6))
U38_aaaag(X1, X2, X3, X4, X5, X6, appcE_out_aaaag(X2, X3, X4, X5, X6)) → appcE_out_aaaag(cons(X1, X2), X3, X4, X5, cons(X1, X6))
appcF_in_gggga(nil, X1, X2, X3, cons(s(a, s(X1, X2), b), X3)) → appcF_out_gggga(nil, X1, X2, X3, cons(s(a, s(X1, X2), b), X3))
appcF_in_gggga(cons(X1, X2), X3, X4, X5, cons(X1, X6)) → U39_gggga(X1, X2, X3, X4, X5, X6, appcF_in_gggga(X2, X3, X4, X5, X6))
U39_gggga(X1, X2, X3, X4, X5, X6, appcF_out_gggga(X2, X3, X4, X5, X6)) → appcF_out_gggga(cons(X1, X2), X3, X4, X5, cons(X1, X6))
appcG_in_aag(nil, X1, cons(a, cons(b, X1))) → appcG_out_aag(nil, X1, cons(a, cons(b, X1)))
appcG_in_aag(cons(X1, X2), X3, cons(X1, X4)) → U40_aag(X1, X2, X3, X4, appcG_in_aag(X2, X3, X4))
U40_aag(X1, X2, X3, X4, appcG_out_aag(X2, X3, X4)) → appcG_out_aag(cons(X1, X2), X3, cons(X1, X4))
appcH_in_gga(nil, X1, cons(s(a, b), X1)) → appcH_out_gga(nil, X1, cons(s(a, b), X1))
appcH_in_gga(cons(X1, X2), X3, cons(X1, X4)) → U41_gga(X1, X2, X3, X4, appcH_in_gga(X2, X3, X4))
U41_gga(X1, X2, X3, X4, appcH_out_gga(X2, X3, X4)) → appcH_out_gga(cons(X1, X2), X3, cons(X1, X4))

The argument filtering Pi contains the following mapping:
cons(x1, x2)  =  cons(x1, x2)
a  =  a
s(x1, x2, x3)  =  s(x1, x2, x3)
b  =  b
appcB_in_gggga(x1, x2, x3, x4, x5)  =  appcB_in_gggga(x1, x2, x3, x4)
appcB_out_gggga(x1, x2, x3, x4, x5)  =  appcB_out_gggga(x1, x2, x3, x4, x5)
appcC_in_aaaaag(x1, x2, x3, x4, x5, x6)  =  appcC_in_aaaaag(x6)
appcC_out_aaaaag(x1, x2, x3, x4, x5, x6)  =  appcC_out_aaaaag(x1, x2, x3, x4, x5, x6)
U36_aaaaag(x1, x2, x3, x4, x5, x6, x7, x8)  =  U36_aaaaag(x1, x7, x8)
appcD_in_gggggga(x1, x2, x3, x4, x5, x6, x7)  =  appcD_in_gggggga(x1, x2, x3, x4, x5, x6)
U42_gggggga(x1, x2, x3, x4, x5, x6, x7, x8)  =  U42_gggggga(x1, x2, x3, x4, x5, x6, x8)
appcI_in_ggggga(x1, x2, x3, x4, x5, x6)  =  appcI_in_ggggga(x1, x2, x3, x4, x5)
nil  =  nil
appcI_out_ggggga(x1, x2, x3, x4, x5, x6)  =  appcI_out_ggggga(x1, x2, x3, x4, x5, x6)
U37_ggggga(x1, x2, x3, x4, x5, x6, x7, x8)  =  U37_ggggga(x1, x2, x3, x4, x5, x6, x8)
appcD_out_gggggga(x1, x2, x3, x4, x5, x6, x7)  =  appcD_out_gggggga(x1, x2, x3, x4, x5, x6, x7)
appcE_in_aaaag(x1, x2, x3, x4, x5)  =  appcE_in_aaaag(x5)
s(x1, x2)  =  s(x1, x2)
appcE_out_aaaag(x1, x2, x3, x4, x5)  =  appcE_out_aaaag(x1, x2, x3, x4, x5)
U38_aaaag(x1, x2, x3, x4, x5, x6, x7)  =  U38_aaaag(x1, x6, x7)
appcF_in_gggga(x1, x2, x3, x4, x5)  =  appcF_in_gggga(x1, x2, x3, x4)
appcF_out_gggga(x1, x2, x3, x4, x5)  =  appcF_out_gggga(x1, x2, x3, x4, x5)
U39_gggga(x1, x2, x3, x4, x5, x6, x7)  =  U39_gggga(x1, x2, x3, x4, x5, x7)
appcG_in_aag(x1, x2, x3)  =  appcG_in_aag(x3)
appcG_out_aag(x1, x2, x3)  =  appcG_out_aag(x1, x2, x3)
U40_aag(x1, x2, x3, x4, x5)  =  U40_aag(x1, x4, x5)
appcH_in_gga(x1, x2, x3)  =  appcH_in_gga(x1, x2)
appcH_out_gga(x1, x2, x3)  =  appcH_out_gga(x1, x2, x3)
U41_gga(x1, x2, x3, x4, x5)  =  U41_gga(x1, x2, x3, x5)
APPH_IN_GGA(x1, x2, x3)  =  APPH_IN_GGA(x1, x2)

We have to consider all (P,R,Pi)-chains

(8) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(9) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

APPH_IN_GGA(cons(X1, X2), X3, cons(X1, X4)) → APPH_IN_GGA(X2, X3, X4)

R is empty.
The argument filtering Pi contains the following mapping:
cons(x1, x2)  =  cons(x1, x2)
APPH_IN_GGA(x1, x2, x3)  =  APPH_IN_GGA(x1, x2)

We have to consider all (P,R,Pi)-chains

(10) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(11) Obligation:

Q DP problem:
The TRS P consists of the following rules:

APPH_IN_GGA(cons(X1, X2), X3) → APPH_IN_GGA(X2, X3)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(12) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • APPH_IN_GGA(cons(X1, X2), X3) → APPH_IN_GGA(X2, X3)
    The graph contains the following edges 1 > 1, 2 >= 2

(13) YES

(14) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

APPG_IN_AAG(cons(X1, X2), X3, cons(X1, X4)) → APPG_IN_AAG(X2, X3, X4)

The TRS R consists of the following rules:

appcB_in_gggga(X1, X2, X3, X4, cons(s(a, s(X1, X2, X3), b), X4)) → appcB_out_gggga(X1, X2, X3, X4, cons(s(a, s(X1, X2, X3), b), X4))
appcC_in_aaaaag(nil, X1, X2, X3, X4, cons(a, cons(s(X1, X2, X3), cons(b, X4)))) → appcC_out_aaaaag(nil, X1, X2, X3, X4, cons(a, cons(s(X1, X2, X3), cons(b, X4))))
appcC_in_aaaaag(cons(X1, X2), X3, X4, X5, X6, cons(X1, X7)) → U36_aaaaag(X1, X2, X3, X4, X5, X6, X7, appcC_in_aaaaag(X2, X3, X4, X5, X6, X7))
U36_aaaaag(X1, X2, X3, X4, X5, X6, X7, appcC_out_aaaaag(X2, X3, X4, X5, X6, X7)) → appcC_out_aaaaag(cons(X1, X2), X3, X4, X5, X6, cons(X1, X7))
appcD_in_gggggga(X1, X2, X3, X4, X5, X6, cons(X1, X7)) → U42_gggggga(X1, X2, X3, X4, X5, X6, X7, appcI_in_ggggga(X2, X3, X4, X5, X6, X7))
appcI_in_ggggga(nil, X1, X2, X3, X4, cons(s(a, s(X1, X2, X3), b), X4)) → appcI_out_ggggga(nil, X1, X2, X3, X4, cons(s(a, s(X1, X2, X3), b), X4))
appcI_in_ggggga(cons(X1, X2), X3, X4, X5, X6, cons(X1, X7)) → U37_ggggga(X1, X2, X3, X4, X5, X6, X7, appcI_in_ggggga(X2, X3, X4, X5, X6, X7))
U37_ggggga(X1, X2, X3, X4, X5, X6, X7, appcI_out_ggggga(X2, X3, X4, X5, X6, X7)) → appcI_out_ggggga(cons(X1, X2), X3, X4, X5, X6, cons(X1, X7))
U42_gggggga(X1, X2, X3, X4, X5, X6, X7, appcI_out_ggggga(X2, X3, X4, X5, X6, X7)) → appcD_out_gggggga(X1, X2, X3, X4, X5, X6, cons(X1, X7))
appcE_in_aaaag(nil, X1, X2, X3, cons(a, cons(s(X1, X2), cons(b, X3)))) → appcE_out_aaaag(nil, X1, X2, X3, cons(a, cons(s(X1, X2), cons(b, X3))))
appcE_in_aaaag(cons(X1, X2), X3, X4, X5, cons(X1, X6)) → U38_aaaag(X1, X2, X3, X4, X5, X6, appcE_in_aaaag(X2, X3, X4, X5, X6))
U38_aaaag(X1, X2, X3, X4, X5, X6, appcE_out_aaaag(X2, X3, X4, X5, X6)) → appcE_out_aaaag(cons(X1, X2), X3, X4, X5, cons(X1, X6))
appcF_in_gggga(nil, X1, X2, X3, cons(s(a, s(X1, X2), b), X3)) → appcF_out_gggga(nil, X1, X2, X3, cons(s(a, s(X1, X2), b), X3))
appcF_in_gggga(cons(X1, X2), X3, X4, X5, cons(X1, X6)) → U39_gggga(X1, X2, X3, X4, X5, X6, appcF_in_gggga(X2, X3, X4, X5, X6))
U39_gggga(X1, X2, X3, X4, X5, X6, appcF_out_gggga(X2, X3, X4, X5, X6)) → appcF_out_gggga(cons(X1, X2), X3, X4, X5, cons(X1, X6))
appcG_in_aag(nil, X1, cons(a, cons(b, X1))) → appcG_out_aag(nil, X1, cons(a, cons(b, X1)))
appcG_in_aag(cons(X1, X2), X3, cons(X1, X4)) → U40_aag(X1, X2, X3, X4, appcG_in_aag(X2, X3, X4))
U40_aag(X1, X2, X3, X4, appcG_out_aag(X2, X3, X4)) → appcG_out_aag(cons(X1, X2), X3, cons(X1, X4))
appcH_in_gga(nil, X1, cons(s(a, b), X1)) → appcH_out_gga(nil, X1, cons(s(a, b), X1))
appcH_in_gga(cons(X1, X2), X3, cons(X1, X4)) → U41_gga(X1, X2, X3, X4, appcH_in_gga(X2, X3, X4))
U41_gga(X1, X2, X3, X4, appcH_out_gga(X2, X3, X4)) → appcH_out_gga(cons(X1, X2), X3, cons(X1, X4))

The argument filtering Pi contains the following mapping:
cons(x1, x2)  =  cons(x1, x2)
a  =  a
s(x1, x2, x3)  =  s(x1, x2, x3)
b  =  b
appcB_in_gggga(x1, x2, x3, x4, x5)  =  appcB_in_gggga(x1, x2, x3, x4)
appcB_out_gggga(x1, x2, x3, x4, x5)  =  appcB_out_gggga(x1, x2, x3, x4, x5)
appcC_in_aaaaag(x1, x2, x3, x4, x5, x6)  =  appcC_in_aaaaag(x6)
appcC_out_aaaaag(x1, x2, x3, x4, x5, x6)  =  appcC_out_aaaaag(x1, x2, x3, x4, x5, x6)
U36_aaaaag(x1, x2, x3, x4, x5, x6, x7, x8)  =  U36_aaaaag(x1, x7, x8)
appcD_in_gggggga(x1, x2, x3, x4, x5, x6, x7)  =  appcD_in_gggggga(x1, x2, x3, x4, x5, x6)
U42_gggggga(x1, x2, x3, x4, x5, x6, x7, x8)  =  U42_gggggga(x1, x2, x3, x4, x5, x6, x8)
appcI_in_ggggga(x1, x2, x3, x4, x5, x6)  =  appcI_in_ggggga(x1, x2, x3, x4, x5)
nil  =  nil
appcI_out_ggggga(x1, x2, x3, x4, x5, x6)  =  appcI_out_ggggga(x1, x2, x3, x4, x5, x6)
U37_ggggga(x1, x2, x3, x4, x5, x6, x7, x8)  =  U37_ggggga(x1, x2, x3, x4, x5, x6, x8)
appcD_out_gggggga(x1, x2, x3, x4, x5, x6, x7)  =  appcD_out_gggggga(x1, x2, x3, x4, x5, x6, x7)
appcE_in_aaaag(x1, x2, x3, x4, x5)  =  appcE_in_aaaag(x5)
s(x1, x2)  =  s(x1, x2)
appcE_out_aaaag(x1, x2, x3, x4, x5)  =  appcE_out_aaaag(x1, x2, x3, x4, x5)
U38_aaaag(x1, x2, x3, x4, x5, x6, x7)  =  U38_aaaag(x1, x6, x7)
appcF_in_gggga(x1, x2, x3, x4, x5)  =  appcF_in_gggga(x1, x2, x3, x4)
appcF_out_gggga(x1, x2, x3, x4, x5)  =  appcF_out_gggga(x1, x2, x3, x4, x5)
U39_gggga(x1, x2, x3, x4, x5, x6, x7)  =  U39_gggga(x1, x2, x3, x4, x5, x7)
appcG_in_aag(x1, x2, x3)  =  appcG_in_aag(x3)
appcG_out_aag(x1, x2, x3)  =  appcG_out_aag(x1, x2, x3)
U40_aag(x1, x2, x3, x4, x5)  =  U40_aag(x1, x4, x5)
appcH_in_gga(x1, x2, x3)  =  appcH_in_gga(x1, x2)
appcH_out_gga(x1, x2, x3)  =  appcH_out_gga(x1, x2, x3)
U41_gga(x1, x2, x3, x4, x5)  =  U41_gga(x1, x2, x3, x5)
APPG_IN_AAG(x1, x2, x3)  =  APPG_IN_AAG(x3)

We have to consider all (P,R,Pi)-chains

(15) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(16) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

APPG_IN_AAG(cons(X1, X2), X3, cons(X1, X4)) → APPG_IN_AAG(X2, X3, X4)

R is empty.
The argument filtering Pi contains the following mapping:
cons(x1, x2)  =  cons(x1, x2)
APPG_IN_AAG(x1, x2, x3)  =  APPG_IN_AAG(x3)

We have to consider all (P,R,Pi)-chains

(17) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(18) Obligation:

Q DP problem:
The TRS P consists of the following rules:

APPG_IN_AAG(cons(X1, X4)) → APPG_IN_AAG(X4)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(19) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • APPG_IN_AAG(cons(X1, X4)) → APPG_IN_AAG(X4)
    The graph contains the following edges 1 > 1

(20) YES

(21) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

APPF_IN_GGGGA(cons(X1, X2), X3, X4, X5, cons(X1, X6)) → APPF_IN_GGGGA(X2, X3, X4, X5, X6)

The TRS R consists of the following rules:

appcB_in_gggga(X1, X2, X3, X4, cons(s(a, s(X1, X2, X3), b), X4)) → appcB_out_gggga(X1, X2, X3, X4, cons(s(a, s(X1, X2, X3), b), X4))
appcC_in_aaaaag(nil, X1, X2, X3, X4, cons(a, cons(s(X1, X2, X3), cons(b, X4)))) → appcC_out_aaaaag(nil, X1, X2, X3, X4, cons(a, cons(s(X1, X2, X3), cons(b, X4))))
appcC_in_aaaaag(cons(X1, X2), X3, X4, X5, X6, cons(X1, X7)) → U36_aaaaag(X1, X2, X3, X4, X5, X6, X7, appcC_in_aaaaag(X2, X3, X4, X5, X6, X7))
U36_aaaaag(X1, X2, X3, X4, X5, X6, X7, appcC_out_aaaaag(X2, X3, X4, X5, X6, X7)) → appcC_out_aaaaag(cons(X1, X2), X3, X4, X5, X6, cons(X1, X7))
appcD_in_gggggga(X1, X2, X3, X4, X5, X6, cons(X1, X7)) → U42_gggggga(X1, X2, X3, X4, X5, X6, X7, appcI_in_ggggga(X2, X3, X4, X5, X6, X7))
appcI_in_ggggga(nil, X1, X2, X3, X4, cons(s(a, s(X1, X2, X3), b), X4)) → appcI_out_ggggga(nil, X1, X2, X3, X4, cons(s(a, s(X1, X2, X3), b), X4))
appcI_in_ggggga(cons(X1, X2), X3, X4, X5, X6, cons(X1, X7)) → U37_ggggga(X1, X2, X3, X4, X5, X6, X7, appcI_in_ggggga(X2, X3, X4, X5, X6, X7))
U37_ggggga(X1, X2, X3, X4, X5, X6, X7, appcI_out_ggggga(X2, X3, X4, X5, X6, X7)) → appcI_out_ggggga(cons(X1, X2), X3, X4, X5, X6, cons(X1, X7))
U42_gggggga(X1, X2, X3, X4, X5, X6, X7, appcI_out_ggggga(X2, X3, X4, X5, X6, X7)) → appcD_out_gggggga(X1, X2, X3, X4, X5, X6, cons(X1, X7))
appcE_in_aaaag(nil, X1, X2, X3, cons(a, cons(s(X1, X2), cons(b, X3)))) → appcE_out_aaaag(nil, X1, X2, X3, cons(a, cons(s(X1, X2), cons(b, X3))))
appcE_in_aaaag(cons(X1, X2), X3, X4, X5, cons(X1, X6)) → U38_aaaag(X1, X2, X3, X4, X5, X6, appcE_in_aaaag(X2, X3, X4, X5, X6))
U38_aaaag(X1, X2, X3, X4, X5, X6, appcE_out_aaaag(X2, X3, X4, X5, X6)) → appcE_out_aaaag(cons(X1, X2), X3, X4, X5, cons(X1, X6))
appcF_in_gggga(nil, X1, X2, X3, cons(s(a, s(X1, X2), b), X3)) → appcF_out_gggga(nil, X1, X2, X3, cons(s(a, s(X1, X2), b), X3))
appcF_in_gggga(cons(X1, X2), X3, X4, X5, cons(X1, X6)) → U39_gggga(X1, X2, X3, X4, X5, X6, appcF_in_gggga(X2, X3, X4, X5, X6))
U39_gggga(X1, X2, X3, X4, X5, X6, appcF_out_gggga(X2, X3, X4, X5, X6)) → appcF_out_gggga(cons(X1, X2), X3, X4, X5, cons(X1, X6))
appcG_in_aag(nil, X1, cons(a, cons(b, X1))) → appcG_out_aag(nil, X1, cons(a, cons(b, X1)))
appcG_in_aag(cons(X1, X2), X3, cons(X1, X4)) → U40_aag(X1, X2, X3, X4, appcG_in_aag(X2, X3, X4))
U40_aag(X1, X2, X3, X4, appcG_out_aag(X2, X3, X4)) → appcG_out_aag(cons(X1, X2), X3, cons(X1, X4))
appcH_in_gga(nil, X1, cons(s(a, b), X1)) → appcH_out_gga(nil, X1, cons(s(a, b), X1))
appcH_in_gga(cons(X1, X2), X3, cons(X1, X4)) → U41_gga(X1, X2, X3, X4, appcH_in_gga(X2, X3, X4))
U41_gga(X1, X2, X3, X4, appcH_out_gga(X2, X3, X4)) → appcH_out_gga(cons(X1, X2), X3, cons(X1, X4))

The argument filtering Pi contains the following mapping:
cons(x1, x2)  =  cons(x1, x2)
a  =  a
s(x1, x2, x3)  =  s(x1, x2, x3)
b  =  b
appcB_in_gggga(x1, x2, x3, x4, x5)  =  appcB_in_gggga(x1, x2, x3, x4)
appcB_out_gggga(x1, x2, x3, x4, x5)  =  appcB_out_gggga(x1, x2, x3, x4, x5)
appcC_in_aaaaag(x1, x2, x3, x4, x5, x6)  =  appcC_in_aaaaag(x6)
appcC_out_aaaaag(x1, x2, x3, x4, x5, x6)  =  appcC_out_aaaaag(x1, x2, x3, x4, x5, x6)
U36_aaaaag(x1, x2, x3, x4, x5, x6, x7, x8)  =  U36_aaaaag(x1, x7, x8)
appcD_in_gggggga(x1, x2, x3, x4, x5, x6, x7)  =  appcD_in_gggggga(x1, x2, x3, x4, x5, x6)
U42_gggggga(x1, x2, x3, x4, x5, x6, x7, x8)  =  U42_gggggga(x1, x2, x3, x4, x5, x6, x8)
appcI_in_ggggga(x1, x2, x3, x4, x5, x6)  =  appcI_in_ggggga(x1, x2, x3, x4, x5)
nil  =  nil
appcI_out_ggggga(x1, x2, x3, x4, x5, x6)  =  appcI_out_ggggga(x1, x2, x3, x4, x5, x6)
U37_ggggga(x1, x2, x3, x4, x5, x6, x7, x8)  =  U37_ggggga(x1, x2, x3, x4, x5, x6, x8)
appcD_out_gggggga(x1, x2, x3, x4, x5, x6, x7)  =  appcD_out_gggggga(x1, x2, x3, x4, x5, x6, x7)
appcE_in_aaaag(x1, x2, x3, x4, x5)  =  appcE_in_aaaag(x5)
s(x1, x2)  =  s(x1, x2)
appcE_out_aaaag(x1, x2, x3, x4, x5)  =  appcE_out_aaaag(x1, x2, x3, x4, x5)
U38_aaaag(x1, x2, x3, x4, x5, x6, x7)  =  U38_aaaag(x1, x6, x7)
appcF_in_gggga(x1, x2, x3, x4, x5)  =  appcF_in_gggga(x1, x2, x3, x4)
appcF_out_gggga(x1, x2, x3, x4, x5)  =  appcF_out_gggga(x1, x2, x3, x4, x5)
U39_gggga(x1, x2, x3, x4, x5, x6, x7)  =  U39_gggga(x1, x2, x3, x4, x5, x7)
appcG_in_aag(x1, x2, x3)  =  appcG_in_aag(x3)
appcG_out_aag(x1, x2, x3)  =  appcG_out_aag(x1, x2, x3)
U40_aag(x1, x2, x3, x4, x5)  =  U40_aag(x1, x4, x5)
appcH_in_gga(x1, x2, x3)  =  appcH_in_gga(x1, x2)
appcH_out_gga(x1, x2, x3)  =  appcH_out_gga(x1, x2, x3)
U41_gga(x1, x2, x3, x4, x5)  =  U41_gga(x1, x2, x3, x5)
APPF_IN_GGGGA(x1, x2, x3, x4, x5)  =  APPF_IN_GGGGA(x1, x2, x3, x4)

We have to consider all (P,R,Pi)-chains

(22) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(23) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

APPF_IN_GGGGA(cons(X1, X2), X3, X4, X5, cons(X1, X6)) → APPF_IN_GGGGA(X2, X3, X4, X5, X6)

R is empty.
The argument filtering Pi contains the following mapping:
cons(x1, x2)  =  cons(x1, x2)
APPF_IN_GGGGA(x1, x2, x3, x4, x5)  =  APPF_IN_GGGGA(x1, x2, x3, x4)

We have to consider all (P,R,Pi)-chains

(24) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(25) Obligation:

Q DP problem:
The TRS P consists of the following rules:

APPF_IN_GGGGA(cons(X1, X2), X3, X4, X5) → APPF_IN_GGGGA(X2, X3, X4, X5)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(26) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • APPF_IN_GGGGA(cons(X1, X2), X3, X4, X5) → APPF_IN_GGGGA(X2, X3, X4, X5)
    The graph contains the following edges 1 > 1, 2 >= 2, 3 >= 3, 4 >= 4

(27) YES

(28) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

APPE_IN_AAAAG(cons(X1, X2), X3, X4, X5, cons(X1, X6)) → APPE_IN_AAAAG(X2, X3, X4, X5, X6)

The TRS R consists of the following rules:

appcB_in_gggga(X1, X2, X3, X4, cons(s(a, s(X1, X2, X3), b), X4)) → appcB_out_gggga(X1, X2, X3, X4, cons(s(a, s(X1, X2, X3), b), X4))
appcC_in_aaaaag(nil, X1, X2, X3, X4, cons(a, cons(s(X1, X2, X3), cons(b, X4)))) → appcC_out_aaaaag(nil, X1, X2, X3, X4, cons(a, cons(s(X1, X2, X3), cons(b, X4))))
appcC_in_aaaaag(cons(X1, X2), X3, X4, X5, X6, cons(X1, X7)) → U36_aaaaag(X1, X2, X3, X4, X5, X6, X7, appcC_in_aaaaag(X2, X3, X4, X5, X6, X7))
U36_aaaaag(X1, X2, X3, X4, X5, X6, X7, appcC_out_aaaaag(X2, X3, X4, X5, X6, X7)) → appcC_out_aaaaag(cons(X1, X2), X3, X4, X5, X6, cons(X1, X7))
appcD_in_gggggga(X1, X2, X3, X4, X5, X6, cons(X1, X7)) → U42_gggggga(X1, X2, X3, X4, X5, X6, X7, appcI_in_ggggga(X2, X3, X4, X5, X6, X7))
appcI_in_ggggga(nil, X1, X2, X3, X4, cons(s(a, s(X1, X2, X3), b), X4)) → appcI_out_ggggga(nil, X1, X2, X3, X4, cons(s(a, s(X1, X2, X3), b), X4))
appcI_in_ggggga(cons(X1, X2), X3, X4, X5, X6, cons(X1, X7)) → U37_ggggga(X1, X2, X3, X4, X5, X6, X7, appcI_in_ggggga(X2, X3, X4, X5, X6, X7))
U37_ggggga(X1, X2, X3, X4, X5, X6, X7, appcI_out_ggggga(X2, X3, X4, X5, X6, X7)) → appcI_out_ggggga(cons(X1, X2), X3, X4, X5, X6, cons(X1, X7))
U42_gggggga(X1, X2, X3, X4, X5, X6, X7, appcI_out_ggggga(X2, X3, X4, X5, X6, X7)) → appcD_out_gggggga(X1, X2, X3, X4, X5, X6, cons(X1, X7))
appcE_in_aaaag(nil, X1, X2, X3, cons(a, cons(s(X1, X2), cons(b, X3)))) → appcE_out_aaaag(nil, X1, X2, X3, cons(a, cons(s(X1, X2), cons(b, X3))))
appcE_in_aaaag(cons(X1, X2), X3, X4, X5, cons(X1, X6)) → U38_aaaag(X1, X2, X3, X4, X5, X6, appcE_in_aaaag(X2, X3, X4, X5, X6))
U38_aaaag(X1, X2, X3, X4, X5, X6, appcE_out_aaaag(X2, X3, X4, X5, X6)) → appcE_out_aaaag(cons(X1, X2), X3, X4, X5, cons(X1, X6))
appcF_in_gggga(nil, X1, X2, X3, cons(s(a, s(X1, X2), b), X3)) → appcF_out_gggga(nil, X1, X2, X3, cons(s(a, s(X1, X2), b), X3))
appcF_in_gggga(cons(X1, X2), X3, X4, X5, cons(X1, X6)) → U39_gggga(X1, X2, X3, X4, X5, X6, appcF_in_gggga(X2, X3, X4, X5, X6))
U39_gggga(X1, X2, X3, X4, X5, X6, appcF_out_gggga(X2, X3, X4, X5, X6)) → appcF_out_gggga(cons(X1, X2), X3, X4, X5, cons(X1, X6))
appcG_in_aag(nil, X1, cons(a, cons(b, X1))) → appcG_out_aag(nil, X1, cons(a, cons(b, X1)))
appcG_in_aag(cons(X1, X2), X3, cons(X1, X4)) → U40_aag(X1, X2, X3, X4, appcG_in_aag(X2, X3, X4))
U40_aag(X1, X2, X3, X4, appcG_out_aag(X2, X3, X4)) → appcG_out_aag(cons(X1, X2), X3, cons(X1, X4))
appcH_in_gga(nil, X1, cons(s(a, b), X1)) → appcH_out_gga(nil, X1, cons(s(a, b), X1))
appcH_in_gga(cons(X1, X2), X3, cons(X1, X4)) → U41_gga(X1, X2, X3, X4, appcH_in_gga(X2, X3, X4))
U41_gga(X1, X2, X3, X4, appcH_out_gga(X2, X3, X4)) → appcH_out_gga(cons(X1, X2), X3, cons(X1, X4))

The argument filtering Pi contains the following mapping:
cons(x1, x2)  =  cons(x1, x2)
a  =  a
s(x1, x2, x3)  =  s(x1, x2, x3)
b  =  b
appcB_in_gggga(x1, x2, x3, x4, x5)  =  appcB_in_gggga(x1, x2, x3, x4)
appcB_out_gggga(x1, x2, x3, x4, x5)  =  appcB_out_gggga(x1, x2, x3, x4, x5)
appcC_in_aaaaag(x1, x2, x3, x4, x5, x6)  =  appcC_in_aaaaag(x6)
appcC_out_aaaaag(x1, x2, x3, x4, x5, x6)  =  appcC_out_aaaaag(x1, x2, x3, x4, x5, x6)
U36_aaaaag(x1, x2, x3, x4, x5, x6, x7, x8)  =  U36_aaaaag(x1, x7, x8)
appcD_in_gggggga(x1, x2, x3, x4, x5, x6, x7)  =  appcD_in_gggggga(x1, x2, x3, x4, x5, x6)
U42_gggggga(x1, x2, x3, x4, x5, x6, x7, x8)  =  U42_gggggga(x1, x2, x3, x4, x5, x6, x8)
appcI_in_ggggga(x1, x2, x3, x4, x5, x6)  =  appcI_in_ggggga(x1, x2, x3, x4, x5)
nil  =  nil
appcI_out_ggggga(x1, x2, x3, x4, x5, x6)  =  appcI_out_ggggga(x1, x2, x3, x4, x5, x6)
U37_ggggga(x1, x2, x3, x4, x5, x6, x7, x8)  =  U37_ggggga(x1, x2, x3, x4, x5, x6, x8)
appcD_out_gggggga(x1, x2, x3, x4, x5, x6, x7)  =  appcD_out_gggggga(x1, x2, x3, x4, x5, x6, x7)
appcE_in_aaaag(x1, x2, x3, x4, x5)  =  appcE_in_aaaag(x5)
s(x1, x2)  =  s(x1, x2)
appcE_out_aaaag(x1, x2, x3, x4, x5)  =  appcE_out_aaaag(x1, x2, x3, x4, x5)
U38_aaaag(x1, x2, x3, x4, x5, x6, x7)  =  U38_aaaag(x1, x6, x7)
appcF_in_gggga(x1, x2, x3, x4, x5)  =  appcF_in_gggga(x1, x2, x3, x4)
appcF_out_gggga(x1, x2, x3, x4, x5)  =  appcF_out_gggga(x1, x2, x3, x4, x5)
U39_gggga(x1, x2, x3, x4, x5, x6, x7)  =  U39_gggga(x1, x2, x3, x4, x5, x7)
appcG_in_aag(x1, x2, x3)  =  appcG_in_aag(x3)
appcG_out_aag(x1, x2, x3)  =  appcG_out_aag(x1, x2, x3)
U40_aag(x1, x2, x3, x4, x5)  =  U40_aag(x1, x4, x5)
appcH_in_gga(x1, x2, x3)  =  appcH_in_gga(x1, x2)
appcH_out_gga(x1, x2, x3)  =  appcH_out_gga(x1, x2, x3)
U41_gga(x1, x2, x3, x4, x5)  =  U41_gga(x1, x2, x3, x5)
APPE_IN_AAAAG(x1, x2, x3, x4, x5)  =  APPE_IN_AAAAG(x5)

We have to consider all (P,R,Pi)-chains

(29) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(30) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

APPE_IN_AAAAG(cons(X1, X2), X3, X4, X5, cons(X1, X6)) → APPE_IN_AAAAG(X2, X3, X4, X5, X6)

R is empty.
The argument filtering Pi contains the following mapping:
cons(x1, x2)  =  cons(x1, x2)
APPE_IN_AAAAG(x1, x2, x3, x4, x5)  =  APPE_IN_AAAAG(x5)

We have to consider all (P,R,Pi)-chains

(31) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(32) Obligation:

Q DP problem:
The TRS P consists of the following rules:

APPE_IN_AAAAG(cons(X1, X6)) → APPE_IN_AAAAG(X6)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(33) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • APPE_IN_AAAAG(cons(X1, X6)) → APPE_IN_AAAAG(X6)
    The graph contains the following edges 1 > 1

(34) YES

(35) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

APPI_IN_GGGGGA(cons(X1, X2), X3, X4, X5, X6, cons(X1, X7)) → APPI_IN_GGGGGA(X2, X3, X4, X5, X6, X7)

The TRS R consists of the following rules:

appcB_in_gggga(X1, X2, X3, X4, cons(s(a, s(X1, X2, X3), b), X4)) → appcB_out_gggga(X1, X2, X3, X4, cons(s(a, s(X1, X2, X3), b), X4))
appcC_in_aaaaag(nil, X1, X2, X3, X4, cons(a, cons(s(X1, X2, X3), cons(b, X4)))) → appcC_out_aaaaag(nil, X1, X2, X3, X4, cons(a, cons(s(X1, X2, X3), cons(b, X4))))
appcC_in_aaaaag(cons(X1, X2), X3, X4, X5, X6, cons(X1, X7)) → U36_aaaaag(X1, X2, X3, X4, X5, X6, X7, appcC_in_aaaaag(X2, X3, X4, X5, X6, X7))
U36_aaaaag(X1, X2, X3, X4, X5, X6, X7, appcC_out_aaaaag(X2, X3, X4, X5, X6, X7)) → appcC_out_aaaaag(cons(X1, X2), X3, X4, X5, X6, cons(X1, X7))
appcD_in_gggggga(X1, X2, X3, X4, X5, X6, cons(X1, X7)) → U42_gggggga(X1, X2, X3, X4, X5, X6, X7, appcI_in_ggggga(X2, X3, X4, X5, X6, X7))
appcI_in_ggggga(nil, X1, X2, X3, X4, cons(s(a, s(X1, X2, X3), b), X4)) → appcI_out_ggggga(nil, X1, X2, X3, X4, cons(s(a, s(X1, X2, X3), b), X4))
appcI_in_ggggga(cons(X1, X2), X3, X4, X5, X6, cons(X1, X7)) → U37_ggggga(X1, X2, X3, X4, X5, X6, X7, appcI_in_ggggga(X2, X3, X4, X5, X6, X7))
U37_ggggga(X1, X2, X3, X4, X5, X6, X7, appcI_out_ggggga(X2, X3, X4, X5, X6, X7)) → appcI_out_ggggga(cons(X1, X2), X3, X4, X5, X6, cons(X1, X7))
U42_gggggga(X1, X2, X3, X4, X5, X6, X7, appcI_out_ggggga(X2, X3, X4, X5, X6, X7)) → appcD_out_gggggga(X1, X2, X3, X4, X5, X6, cons(X1, X7))
appcE_in_aaaag(nil, X1, X2, X3, cons(a, cons(s(X1, X2), cons(b, X3)))) → appcE_out_aaaag(nil, X1, X2, X3, cons(a, cons(s(X1, X2), cons(b, X3))))
appcE_in_aaaag(cons(X1, X2), X3, X4, X5, cons(X1, X6)) → U38_aaaag(X1, X2, X3, X4, X5, X6, appcE_in_aaaag(X2, X3, X4, X5, X6))
U38_aaaag(X1, X2, X3, X4, X5, X6, appcE_out_aaaag(X2, X3, X4, X5, X6)) → appcE_out_aaaag(cons(X1, X2), X3, X4, X5, cons(X1, X6))
appcF_in_gggga(nil, X1, X2, X3, cons(s(a, s(X1, X2), b), X3)) → appcF_out_gggga(nil, X1, X2, X3, cons(s(a, s(X1, X2), b), X3))
appcF_in_gggga(cons(X1, X2), X3, X4, X5, cons(X1, X6)) → U39_gggga(X1, X2, X3, X4, X5, X6, appcF_in_gggga(X2, X3, X4, X5, X6))
U39_gggga(X1, X2, X3, X4, X5, X6, appcF_out_gggga(X2, X3, X4, X5, X6)) → appcF_out_gggga(cons(X1, X2), X3, X4, X5, cons(X1, X6))
appcG_in_aag(nil, X1, cons(a, cons(b, X1))) → appcG_out_aag(nil, X1, cons(a, cons(b, X1)))
appcG_in_aag(cons(X1, X2), X3, cons(X1, X4)) → U40_aag(X1, X2, X3, X4, appcG_in_aag(X2, X3, X4))
U40_aag(X1, X2, X3, X4, appcG_out_aag(X2, X3, X4)) → appcG_out_aag(cons(X1, X2), X3, cons(X1, X4))
appcH_in_gga(nil, X1, cons(s(a, b), X1)) → appcH_out_gga(nil, X1, cons(s(a, b), X1))
appcH_in_gga(cons(X1, X2), X3, cons(X1, X4)) → U41_gga(X1, X2, X3, X4, appcH_in_gga(X2, X3, X4))
U41_gga(X1, X2, X3, X4, appcH_out_gga(X2, X3, X4)) → appcH_out_gga(cons(X1, X2), X3, cons(X1, X4))

The argument filtering Pi contains the following mapping:
cons(x1, x2)  =  cons(x1, x2)
a  =  a
s(x1, x2, x3)  =  s(x1, x2, x3)
b  =  b
appcB_in_gggga(x1, x2, x3, x4, x5)  =  appcB_in_gggga(x1, x2, x3, x4)
appcB_out_gggga(x1, x2, x3, x4, x5)  =  appcB_out_gggga(x1, x2, x3, x4, x5)
appcC_in_aaaaag(x1, x2, x3, x4, x5, x6)  =  appcC_in_aaaaag(x6)
appcC_out_aaaaag(x1, x2, x3, x4, x5, x6)  =  appcC_out_aaaaag(x1, x2, x3, x4, x5, x6)
U36_aaaaag(x1, x2, x3, x4, x5, x6, x7, x8)  =  U36_aaaaag(x1, x7, x8)
appcD_in_gggggga(x1, x2, x3, x4, x5, x6, x7)  =  appcD_in_gggggga(x1, x2, x3, x4, x5, x6)
U42_gggggga(x1, x2, x3, x4, x5, x6, x7, x8)  =  U42_gggggga(x1, x2, x3, x4, x5, x6, x8)
appcI_in_ggggga(x1, x2, x3, x4, x5, x6)  =  appcI_in_ggggga(x1, x2, x3, x4, x5)
nil  =  nil
appcI_out_ggggga(x1, x2, x3, x4, x5, x6)  =  appcI_out_ggggga(x1, x2, x3, x4, x5, x6)
U37_ggggga(x1, x2, x3, x4, x5, x6, x7, x8)  =  U37_ggggga(x1, x2, x3, x4, x5, x6, x8)
appcD_out_gggggga(x1, x2, x3, x4, x5, x6, x7)  =  appcD_out_gggggga(x1, x2, x3, x4, x5, x6, x7)
appcE_in_aaaag(x1, x2, x3, x4, x5)  =  appcE_in_aaaag(x5)
s(x1, x2)  =  s(x1, x2)
appcE_out_aaaag(x1, x2, x3, x4, x5)  =  appcE_out_aaaag(x1, x2, x3, x4, x5)
U38_aaaag(x1, x2, x3, x4, x5, x6, x7)  =  U38_aaaag(x1, x6, x7)
appcF_in_gggga(x1, x2, x3, x4, x5)  =  appcF_in_gggga(x1, x2, x3, x4)
appcF_out_gggga(x1, x2, x3, x4, x5)  =  appcF_out_gggga(x1, x2, x3, x4, x5)
U39_gggga(x1, x2, x3, x4, x5, x6, x7)  =  U39_gggga(x1, x2, x3, x4, x5, x7)
appcG_in_aag(x1, x2, x3)  =  appcG_in_aag(x3)
appcG_out_aag(x1, x2, x3)  =  appcG_out_aag(x1, x2, x3)
U40_aag(x1, x2, x3, x4, x5)  =  U40_aag(x1, x4, x5)
appcH_in_gga(x1, x2, x3)  =  appcH_in_gga(x1, x2)
appcH_out_gga(x1, x2, x3)  =  appcH_out_gga(x1, x2, x3)
U41_gga(x1, x2, x3, x4, x5)  =  U41_gga(x1, x2, x3, x5)
APPI_IN_GGGGGA(x1, x2, x3, x4, x5, x6)  =  APPI_IN_GGGGGA(x1, x2, x3, x4, x5)

We have to consider all (P,R,Pi)-chains

(36) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(37) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

APPI_IN_GGGGGA(cons(X1, X2), X3, X4, X5, X6, cons(X1, X7)) → APPI_IN_GGGGGA(X2, X3, X4, X5, X6, X7)

R is empty.
The argument filtering Pi contains the following mapping:
cons(x1, x2)  =  cons(x1, x2)
APPI_IN_GGGGGA(x1, x2, x3, x4, x5, x6)  =  APPI_IN_GGGGGA(x1, x2, x3, x4, x5)

We have to consider all (P,R,Pi)-chains

(38) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(39) Obligation:

Q DP problem:
The TRS P consists of the following rules:

APPI_IN_GGGGGA(cons(X1, X2), X3, X4, X5, X6) → APPI_IN_GGGGGA(X2, X3, X4, X5, X6)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(40) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • APPI_IN_GGGGGA(cons(X1, X2), X3, X4, X5, X6) → APPI_IN_GGGGGA(X2, X3, X4, X5, X6)
    The graph contains the following edges 1 > 1, 2 >= 2, 3 >= 3, 4 >= 4, 5 >= 5

(41) YES

(42) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

APPC_IN_AAAAAG(cons(X1, X2), X3, X4, X5, X6, cons(X1, X7)) → APPC_IN_AAAAAG(X2, X3, X4, X5, X6, X7)

The TRS R consists of the following rules:

appcB_in_gggga(X1, X2, X3, X4, cons(s(a, s(X1, X2, X3), b), X4)) → appcB_out_gggga(X1, X2, X3, X4, cons(s(a, s(X1, X2, X3), b), X4))
appcC_in_aaaaag(nil, X1, X2, X3, X4, cons(a, cons(s(X1, X2, X3), cons(b, X4)))) → appcC_out_aaaaag(nil, X1, X2, X3, X4, cons(a, cons(s(X1, X2, X3), cons(b, X4))))
appcC_in_aaaaag(cons(X1, X2), X3, X4, X5, X6, cons(X1, X7)) → U36_aaaaag(X1, X2, X3, X4, X5, X6, X7, appcC_in_aaaaag(X2, X3, X4, X5, X6, X7))
U36_aaaaag(X1, X2, X3, X4, X5, X6, X7, appcC_out_aaaaag(X2, X3, X4, X5, X6, X7)) → appcC_out_aaaaag(cons(X1, X2), X3, X4, X5, X6, cons(X1, X7))
appcD_in_gggggga(X1, X2, X3, X4, X5, X6, cons(X1, X7)) → U42_gggggga(X1, X2, X3, X4, X5, X6, X7, appcI_in_ggggga(X2, X3, X4, X5, X6, X7))
appcI_in_ggggga(nil, X1, X2, X3, X4, cons(s(a, s(X1, X2, X3), b), X4)) → appcI_out_ggggga(nil, X1, X2, X3, X4, cons(s(a, s(X1, X2, X3), b), X4))
appcI_in_ggggga(cons(X1, X2), X3, X4, X5, X6, cons(X1, X7)) → U37_ggggga(X1, X2, X3, X4, X5, X6, X7, appcI_in_ggggga(X2, X3, X4, X5, X6, X7))
U37_ggggga(X1, X2, X3, X4, X5, X6, X7, appcI_out_ggggga(X2, X3, X4, X5, X6, X7)) → appcI_out_ggggga(cons(X1, X2), X3, X4, X5, X6, cons(X1, X7))
U42_gggggga(X1, X2, X3, X4, X5, X6, X7, appcI_out_ggggga(X2, X3, X4, X5, X6, X7)) → appcD_out_gggggga(X1, X2, X3, X4, X5, X6, cons(X1, X7))
appcE_in_aaaag(nil, X1, X2, X3, cons(a, cons(s(X1, X2), cons(b, X3)))) → appcE_out_aaaag(nil, X1, X2, X3, cons(a, cons(s(X1, X2), cons(b, X3))))
appcE_in_aaaag(cons(X1, X2), X3, X4, X5, cons(X1, X6)) → U38_aaaag(X1, X2, X3, X4, X5, X6, appcE_in_aaaag(X2, X3, X4, X5, X6))
U38_aaaag(X1, X2, X3, X4, X5, X6, appcE_out_aaaag(X2, X3, X4, X5, X6)) → appcE_out_aaaag(cons(X1, X2), X3, X4, X5, cons(X1, X6))
appcF_in_gggga(nil, X1, X2, X3, cons(s(a, s(X1, X2), b), X3)) → appcF_out_gggga(nil, X1, X2, X3, cons(s(a, s(X1, X2), b), X3))
appcF_in_gggga(cons(X1, X2), X3, X4, X5, cons(X1, X6)) → U39_gggga(X1, X2, X3, X4, X5, X6, appcF_in_gggga(X2, X3, X4, X5, X6))
U39_gggga(X1, X2, X3, X4, X5, X6, appcF_out_gggga(X2, X3, X4, X5, X6)) → appcF_out_gggga(cons(X1, X2), X3, X4, X5, cons(X1, X6))
appcG_in_aag(nil, X1, cons(a, cons(b, X1))) → appcG_out_aag(nil, X1, cons(a, cons(b, X1)))
appcG_in_aag(cons(X1, X2), X3, cons(X1, X4)) → U40_aag(X1, X2, X3, X4, appcG_in_aag(X2, X3, X4))
U40_aag(X1, X2, X3, X4, appcG_out_aag(X2, X3, X4)) → appcG_out_aag(cons(X1, X2), X3, cons(X1, X4))
appcH_in_gga(nil, X1, cons(s(a, b), X1)) → appcH_out_gga(nil, X1, cons(s(a, b), X1))
appcH_in_gga(cons(X1, X2), X3, cons(X1, X4)) → U41_gga(X1, X2, X3, X4, appcH_in_gga(X2, X3, X4))
U41_gga(X1, X2, X3, X4, appcH_out_gga(X2, X3, X4)) → appcH_out_gga(cons(X1, X2), X3, cons(X1, X4))

The argument filtering Pi contains the following mapping:
cons(x1, x2)  =  cons(x1, x2)
a  =  a
s(x1, x2, x3)  =  s(x1, x2, x3)
b  =  b
appcB_in_gggga(x1, x2, x3, x4, x5)  =  appcB_in_gggga(x1, x2, x3, x4)
appcB_out_gggga(x1, x2, x3, x4, x5)  =  appcB_out_gggga(x1, x2, x3, x4, x5)
appcC_in_aaaaag(x1, x2, x3, x4, x5, x6)  =  appcC_in_aaaaag(x6)
appcC_out_aaaaag(x1, x2, x3, x4, x5, x6)  =  appcC_out_aaaaag(x1, x2, x3, x4, x5, x6)
U36_aaaaag(x1, x2, x3, x4, x5, x6, x7, x8)  =  U36_aaaaag(x1, x7, x8)
appcD_in_gggggga(x1, x2, x3, x4, x5, x6, x7)  =  appcD_in_gggggga(x1, x2, x3, x4, x5, x6)
U42_gggggga(x1, x2, x3, x4, x5, x6, x7, x8)  =  U42_gggggga(x1, x2, x3, x4, x5, x6, x8)
appcI_in_ggggga(x1, x2, x3, x4, x5, x6)  =  appcI_in_ggggga(x1, x2, x3, x4, x5)
nil  =  nil
appcI_out_ggggga(x1, x2, x3, x4, x5, x6)  =  appcI_out_ggggga(x1, x2, x3, x4, x5, x6)
U37_ggggga(x1, x2, x3, x4, x5, x6, x7, x8)  =  U37_ggggga(x1, x2, x3, x4, x5, x6, x8)
appcD_out_gggggga(x1, x2, x3, x4, x5, x6, x7)  =  appcD_out_gggggga(x1, x2, x3, x4, x5, x6, x7)
appcE_in_aaaag(x1, x2, x3, x4, x5)  =  appcE_in_aaaag(x5)
s(x1, x2)  =  s(x1, x2)
appcE_out_aaaag(x1, x2, x3, x4, x5)  =  appcE_out_aaaag(x1, x2, x3, x4, x5)
U38_aaaag(x1, x2, x3, x4, x5, x6, x7)  =  U38_aaaag(x1, x6, x7)
appcF_in_gggga(x1, x2, x3, x4, x5)  =  appcF_in_gggga(x1, x2, x3, x4)
appcF_out_gggga(x1, x2, x3, x4, x5)  =  appcF_out_gggga(x1, x2, x3, x4, x5)
U39_gggga(x1, x2, x3, x4, x5, x6, x7)  =  U39_gggga(x1, x2, x3, x4, x5, x7)
appcG_in_aag(x1, x2, x3)  =  appcG_in_aag(x3)
appcG_out_aag(x1, x2, x3)  =  appcG_out_aag(x1, x2, x3)
U40_aag(x1, x2, x3, x4, x5)  =  U40_aag(x1, x4, x5)
appcH_in_gga(x1, x2, x3)  =  appcH_in_gga(x1, x2)
appcH_out_gga(x1, x2, x3)  =  appcH_out_gga(x1, x2, x3)
U41_gga(x1, x2, x3, x4, x5)  =  U41_gga(x1, x2, x3, x5)
APPC_IN_AAAAAG(x1, x2, x3, x4, x5, x6)  =  APPC_IN_AAAAAG(x6)

We have to consider all (P,R,Pi)-chains

(43) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(44) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

APPC_IN_AAAAAG(cons(X1, X2), X3, X4, X5, X6, cons(X1, X7)) → APPC_IN_AAAAAG(X2, X3, X4, X5, X6, X7)

R is empty.
The argument filtering Pi contains the following mapping:
cons(x1, x2)  =  cons(x1, x2)
APPC_IN_AAAAAG(x1, x2, x3, x4, x5, x6)  =  APPC_IN_AAAAAG(x6)

We have to consider all (P,R,Pi)-chains

(45) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(46) Obligation:

Q DP problem:
The TRS P consists of the following rules:

APPC_IN_AAAAAG(cons(X1, X7)) → APPC_IN_AAAAAG(X7)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(47) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • APPC_IN_AAAAAG(cons(X1, X7)) → APPC_IN_AAAAAG(X7)
    The graph contains the following edges 1 > 1

(48) YES

(49) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

U7_GA(X1, X2, X3, X4, X5, appcB_out_gggga(X1, X2, X3, X4, X6)) → PARSEA_IN_GA(X6, X5)
PARSEA_IN_GA(cons(a, cons(s(X1, X2, X3), cons(b, X4))), X5) → U7_GA(X1, X2, X3, X4, X5, appcB_in_gggga(X1, X2, X3, X4, X6))
PARSEA_IN_GA(cons(X1, X2), X3) → U10_GA(X1, X2, X3, appcC_in_aaaaag(X4, X5, X6, X7, X8, X2))
U10_GA(X1, X2, X3, appcC_out_aaaaag(X4, X5, X6, X7, X8, X2)) → U12_GA(X1, X2, X3, appcD_in_gggggga(X1, X4, X5, X6, X7, X8, X9))
U12_GA(X1, X2, X3, appcD_out_gggggga(X1, X4, X5, X6, X7, X8, X9)) → PARSEA_IN_GA(X9, X3)
PARSEA_IN_GA(X1, X2) → U15_GA(X1, X2, appcE_in_aaaag(X3, X4, X5, X6, X1))
U15_GA(X1, X2, appcE_out_aaaag(X3, X4, X5, X6, X1)) → U17_GA(X1, X2, appcF_in_gggga(X3, X4, X5, X6, X7))
U17_GA(X1, X2, appcF_out_gggga(X3, X4, X5, X6, X7)) → PARSEA_IN_GA(X7, X2)
PARSEA_IN_GA(X1, X2) → U20_GA(X1, X2, appcG_in_aag(X3, X4, X1))
U20_GA(X1, X2, appcG_out_aag(X3, X4, X1)) → U22_GA(X1, X2, appcH_in_gga(X3, X4, X5))
U22_GA(X1, X2, appcH_out_gga(X3, X4, X5)) → PARSEA_IN_GA(X5, X2)

The TRS R consists of the following rules:

appcB_in_gggga(X1, X2, X3, X4, cons(s(a, s(X1, X2, X3), b), X4)) → appcB_out_gggga(X1, X2, X3, X4, cons(s(a, s(X1, X2, X3), b), X4))
appcC_in_aaaaag(nil, X1, X2, X3, X4, cons(a, cons(s(X1, X2, X3), cons(b, X4)))) → appcC_out_aaaaag(nil, X1, X2, X3, X4, cons(a, cons(s(X1, X2, X3), cons(b, X4))))
appcC_in_aaaaag(cons(X1, X2), X3, X4, X5, X6, cons(X1, X7)) → U36_aaaaag(X1, X2, X3, X4, X5, X6, X7, appcC_in_aaaaag(X2, X3, X4, X5, X6, X7))
U36_aaaaag(X1, X2, X3, X4, X5, X6, X7, appcC_out_aaaaag(X2, X3, X4, X5, X6, X7)) → appcC_out_aaaaag(cons(X1, X2), X3, X4, X5, X6, cons(X1, X7))
appcD_in_gggggga(X1, X2, X3, X4, X5, X6, cons(X1, X7)) → U42_gggggga(X1, X2, X3, X4, X5, X6, X7, appcI_in_ggggga(X2, X3, X4, X5, X6, X7))
appcI_in_ggggga(nil, X1, X2, X3, X4, cons(s(a, s(X1, X2, X3), b), X4)) → appcI_out_ggggga(nil, X1, X2, X3, X4, cons(s(a, s(X1, X2, X3), b), X4))
appcI_in_ggggga(cons(X1, X2), X3, X4, X5, X6, cons(X1, X7)) → U37_ggggga(X1, X2, X3, X4, X5, X6, X7, appcI_in_ggggga(X2, X3, X4, X5, X6, X7))
U37_ggggga(X1, X2, X3, X4, X5, X6, X7, appcI_out_ggggga(X2, X3, X4, X5, X6, X7)) → appcI_out_ggggga(cons(X1, X2), X3, X4, X5, X6, cons(X1, X7))
U42_gggggga(X1, X2, X3, X4, X5, X6, X7, appcI_out_ggggga(X2, X3, X4, X5, X6, X7)) → appcD_out_gggggga(X1, X2, X3, X4, X5, X6, cons(X1, X7))
appcE_in_aaaag(nil, X1, X2, X3, cons(a, cons(s(X1, X2), cons(b, X3)))) → appcE_out_aaaag(nil, X1, X2, X3, cons(a, cons(s(X1, X2), cons(b, X3))))
appcE_in_aaaag(cons(X1, X2), X3, X4, X5, cons(X1, X6)) → U38_aaaag(X1, X2, X3, X4, X5, X6, appcE_in_aaaag(X2, X3, X4, X5, X6))
U38_aaaag(X1, X2, X3, X4, X5, X6, appcE_out_aaaag(X2, X3, X4, X5, X6)) → appcE_out_aaaag(cons(X1, X2), X3, X4, X5, cons(X1, X6))
appcF_in_gggga(nil, X1, X2, X3, cons(s(a, s(X1, X2), b), X3)) → appcF_out_gggga(nil, X1, X2, X3, cons(s(a, s(X1, X2), b), X3))
appcF_in_gggga(cons(X1, X2), X3, X4, X5, cons(X1, X6)) → U39_gggga(X1, X2, X3, X4, X5, X6, appcF_in_gggga(X2, X3, X4, X5, X6))
U39_gggga(X1, X2, X3, X4, X5, X6, appcF_out_gggga(X2, X3, X4, X5, X6)) → appcF_out_gggga(cons(X1, X2), X3, X4, X5, cons(X1, X6))
appcG_in_aag(nil, X1, cons(a, cons(b, X1))) → appcG_out_aag(nil, X1, cons(a, cons(b, X1)))
appcG_in_aag(cons(X1, X2), X3, cons(X1, X4)) → U40_aag(X1, X2, X3, X4, appcG_in_aag(X2, X3, X4))
U40_aag(X1, X2, X3, X4, appcG_out_aag(X2, X3, X4)) → appcG_out_aag(cons(X1, X2), X3, cons(X1, X4))
appcH_in_gga(nil, X1, cons(s(a, b), X1)) → appcH_out_gga(nil, X1, cons(s(a, b), X1))
appcH_in_gga(cons(X1, X2), X3, cons(X1, X4)) → U41_gga(X1, X2, X3, X4, appcH_in_gga(X2, X3, X4))
U41_gga(X1, X2, X3, X4, appcH_out_gga(X2, X3, X4)) → appcH_out_gga(cons(X1, X2), X3, cons(X1, X4))

The argument filtering Pi contains the following mapping:
cons(x1, x2)  =  cons(x1, x2)
a  =  a
s(x1, x2, x3)  =  s(x1, x2, x3)
b  =  b
appcB_in_gggga(x1, x2, x3, x4, x5)  =  appcB_in_gggga(x1, x2, x3, x4)
appcB_out_gggga(x1, x2, x3, x4, x5)  =  appcB_out_gggga(x1, x2, x3, x4, x5)
appcC_in_aaaaag(x1, x2, x3, x4, x5, x6)  =  appcC_in_aaaaag(x6)
appcC_out_aaaaag(x1, x2, x3, x4, x5, x6)  =  appcC_out_aaaaag(x1, x2, x3, x4, x5, x6)
U36_aaaaag(x1, x2, x3, x4, x5, x6, x7, x8)  =  U36_aaaaag(x1, x7, x8)
appcD_in_gggggga(x1, x2, x3, x4, x5, x6, x7)  =  appcD_in_gggggga(x1, x2, x3, x4, x5, x6)
U42_gggggga(x1, x2, x3, x4, x5, x6, x7, x8)  =  U42_gggggga(x1, x2, x3, x4, x5, x6, x8)
appcI_in_ggggga(x1, x2, x3, x4, x5, x6)  =  appcI_in_ggggga(x1, x2, x3, x4, x5)
nil  =  nil
appcI_out_ggggga(x1, x2, x3, x4, x5, x6)  =  appcI_out_ggggga(x1, x2, x3, x4, x5, x6)
U37_ggggga(x1, x2, x3, x4, x5, x6, x7, x8)  =  U37_ggggga(x1, x2, x3, x4, x5, x6, x8)
appcD_out_gggggga(x1, x2, x3, x4, x5, x6, x7)  =  appcD_out_gggggga(x1, x2, x3, x4, x5, x6, x7)
appcE_in_aaaag(x1, x2, x3, x4, x5)  =  appcE_in_aaaag(x5)
s(x1, x2)  =  s(x1, x2)
appcE_out_aaaag(x1, x2, x3, x4, x5)  =  appcE_out_aaaag(x1, x2, x3, x4, x5)
U38_aaaag(x1, x2, x3, x4, x5, x6, x7)  =  U38_aaaag(x1, x6, x7)
appcF_in_gggga(x1, x2, x3, x4, x5)  =  appcF_in_gggga(x1, x2, x3, x4)
appcF_out_gggga(x1, x2, x3, x4, x5)  =  appcF_out_gggga(x1, x2, x3, x4, x5)
U39_gggga(x1, x2, x3, x4, x5, x6, x7)  =  U39_gggga(x1, x2, x3, x4, x5, x7)
appcG_in_aag(x1, x2, x3)  =  appcG_in_aag(x3)
appcG_out_aag(x1, x2, x3)  =  appcG_out_aag(x1, x2, x3)
U40_aag(x1, x2, x3, x4, x5)  =  U40_aag(x1, x4, x5)
appcH_in_gga(x1, x2, x3)  =  appcH_in_gga(x1, x2)
appcH_out_gga(x1, x2, x3)  =  appcH_out_gga(x1, x2, x3)
U41_gga(x1, x2, x3, x4, x5)  =  U41_gga(x1, x2, x3, x5)
PARSEA_IN_GA(x1, x2)  =  PARSEA_IN_GA(x1)
U7_GA(x1, x2, x3, x4, x5, x6)  =  U7_GA(x1, x2, x3, x4, x6)
U10_GA(x1, x2, x3, x4)  =  U10_GA(x1, x2, x4)
U12_GA(x1, x2, x3, x4)  =  U12_GA(x1, x2, x4)
U15_GA(x1, x2, x3)  =  U15_GA(x1, x3)
U17_GA(x1, x2, x3)  =  U17_GA(x1, x3)
U20_GA(x1, x2, x3)  =  U20_GA(x1, x3)
U22_GA(x1, x2, x3)  =  U22_GA(x1, x3)

We have to consider all (P,R,Pi)-chains

(50) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(51) Obligation:

Q DP problem:
The TRS P consists of the following rules:

U7_GA(X1, X2, X3, X4, appcB_out_gggga(X1, X2, X3, X4, X6)) → PARSEA_IN_GA(X6)
PARSEA_IN_GA(cons(a, cons(s(X1, X2, X3), cons(b, X4)))) → U7_GA(X1, X2, X3, X4, appcB_in_gggga(X1, X2, X3, X4))
PARSEA_IN_GA(cons(X1, X2)) → U10_GA(X1, X2, appcC_in_aaaaag(X2))
U10_GA(X1, X2, appcC_out_aaaaag(X4, X5, X6, X7, X8, X2)) → U12_GA(X1, X2, appcD_in_gggggga(X1, X4, X5, X6, X7, X8))
U12_GA(X1, X2, appcD_out_gggggga(X1, X4, X5, X6, X7, X8, X9)) → PARSEA_IN_GA(X9)
PARSEA_IN_GA(X1) → U15_GA(X1, appcE_in_aaaag(X1))
U15_GA(X1, appcE_out_aaaag(X3, X4, X5, X6, X1)) → U17_GA(X1, appcF_in_gggga(X3, X4, X5, X6))
U17_GA(X1, appcF_out_gggga(X3, X4, X5, X6, X7)) → PARSEA_IN_GA(X7)
PARSEA_IN_GA(X1) → U20_GA(X1, appcG_in_aag(X1))
U20_GA(X1, appcG_out_aag(X3, X4, X1)) → U22_GA(X1, appcH_in_gga(X3, X4))
U22_GA(X1, appcH_out_gga(X3, X4, X5)) → PARSEA_IN_GA(X5)

The TRS R consists of the following rules:

appcB_in_gggga(X1, X2, X3, X4) → appcB_out_gggga(X1, X2, X3, X4, cons(s(a, s(X1, X2, X3), b), X4))
appcC_in_aaaaag(cons(a, cons(s(X1, X2, X3), cons(b, X4)))) → appcC_out_aaaaag(nil, X1, X2, X3, X4, cons(a, cons(s(X1, X2, X3), cons(b, X4))))
appcC_in_aaaaag(cons(X1, X7)) → U36_aaaaag(X1, X7, appcC_in_aaaaag(X7))
U36_aaaaag(X1, X7, appcC_out_aaaaag(X2, X3, X4, X5, X6, X7)) → appcC_out_aaaaag(cons(X1, X2), X3, X4, X5, X6, cons(X1, X7))
appcD_in_gggggga(X1, X2, X3, X4, X5, X6) → U42_gggggga(X1, X2, X3, X4, X5, X6, appcI_in_ggggga(X2, X3, X4, X5, X6))
appcI_in_ggggga(nil, X1, X2, X3, X4) → appcI_out_ggggga(nil, X1, X2, X3, X4, cons(s(a, s(X1, X2, X3), b), X4))
appcI_in_ggggga(cons(X1, X2), X3, X4, X5, X6) → U37_ggggga(X1, X2, X3, X4, X5, X6, appcI_in_ggggga(X2, X3, X4, X5, X6))
U37_ggggga(X1, X2, X3, X4, X5, X6, appcI_out_ggggga(X2, X3, X4, X5, X6, X7)) → appcI_out_ggggga(cons(X1, X2), X3, X4, X5, X6, cons(X1, X7))
U42_gggggga(X1, X2, X3, X4, X5, X6, appcI_out_ggggga(X2, X3, X4, X5, X6, X7)) → appcD_out_gggggga(X1, X2, X3, X4, X5, X6, cons(X1, X7))
appcE_in_aaaag(cons(a, cons(s(X1, X2), cons(b, X3)))) → appcE_out_aaaag(nil, X1, X2, X3, cons(a, cons(s(X1, X2), cons(b, X3))))
appcE_in_aaaag(cons(X1, X6)) → U38_aaaag(X1, X6, appcE_in_aaaag(X6))
U38_aaaag(X1, X6, appcE_out_aaaag(X2, X3, X4, X5, X6)) → appcE_out_aaaag(cons(X1, X2), X3, X4, X5, cons(X1, X6))
appcF_in_gggga(nil, X1, X2, X3) → appcF_out_gggga(nil, X1, X2, X3, cons(s(a, s(X1, X2), b), X3))
appcF_in_gggga(cons(X1, X2), X3, X4, X5) → U39_gggga(X1, X2, X3, X4, X5, appcF_in_gggga(X2, X3, X4, X5))
U39_gggga(X1, X2, X3, X4, X5, appcF_out_gggga(X2, X3, X4, X5, X6)) → appcF_out_gggga(cons(X1, X2), X3, X4, X5, cons(X1, X6))
appcG_in_aag(cons(a, cons(b, X1))) → appcG_out_aag(nil, X1, cons(a, cons(b, X1)))
appcG_in_aag(cons(X1, X4)) → U40_aag(X1, X4, appcG_in_aag(X4))
U40_aag(X1, X4, appcG_out_aag(X2, X3, X4)) → appcG_out_aag(cons(X1, X2), X3, cons(X1, X4))
appcH_in_gga(nil, X1) → appcH_out_gga(nil, X1, cons(s(a, b), X1))
appcH_in_gga(cons(X1, X2), X3) → U41_gga(X1, X2, X3, appcH_in_gga(X2, X3))
U41_gga(X1, X2, X3, appcH_out_gga(X2, X3, X4)) → appcH_out_gga(cons(X1, X2), X3, cons(X1, X4))

The set Q consists of the following terms:

appcB_in_gggga(x0, x1, x2, x3)
appcC_in_aaaaag(x0)
U36_aaaaag(x0, x1, x2)
appcD_in_gggggga(x0, x1, x2, x3, x4, x5)
appcI_in_ggggga(x0, x1, x2, x3, x4)
U37_ggggga(x0, x1, x2, x3, x4, x5, x6)
U42_gggggga(x0, x1, x2, x3, x4, x5, x6)
appcE_in_aaaag(x0)
U38_aaaag(x0, x1, x2)
appcF_in_gggga(x0, x1, x2, x3)
U39_gggga(x0, x1, x2, x3, x4, x5)
appcG_in_aag(x0)
U40_aag(x0, x1, x2)
appcH_in_gga(x0, x1)
U41_gga(x0, x1, x2, x3)

We have to consider all (P,Q,R)-chains.

(52) Rewriting (EQUIVALENT transformation)

By rewriting [LPAR04] the rule PARSEA_IN_GA(cons(a, cons(s(X1, X2, X3), cons(b, X4)))) → U7_GA(X1, X2, X3, X4, appcB_in_gggga(X1, X2, X3, X4)) at position [4] we obtained the following new rules [LPAR04]:

PARSEA_IN_GA(cons(a, cons(s(X1, X2, X3), cons(b, X4)))) → U7_GA(X1, X2, X3, X4, appcB_out_gggga(X1, X2, X3, X4, cons(s(a, s(X1, X2, X3), b), X4)))

(53) Obligation:

Q DP problem:
The TRS P consists of the following rules:

U7_GA(X1, X2, X3, X4, appcB_out_gggga(X1, X2, X3, X4, X6)) → PARSEA_IN_GA(X6)
PARSEA_IN_GA(cons(X1, X2)) → U10_GA(X1, X2, appcC_in_aaaaag(X2))
U10_GA(X1, X2, appcC_out_aaaaag(X4, X5, X6, X7, X8, X2)) → U12_GA(X1, X2, appcD_in_gggggga(X1, X4, X5, X6, X7, X8))
U12_GA(X1, X2, appcD_out_gggggga(X1, X4, X5, X6, X7, X8, X9)) → PARSEA_IN_GA(X9)
PARSEA_IN_GA(X1) → U15_GA(X1, appcE_in_aaaag(X1))
U15_GA(X1, appcE_out_aaaag(X3, X4, X5, X6, X1)) → U17_GA(X1, appcF_in_gggga(X3, X4, X5, X6))
U17_GA(X1, appcF_out_gggga(X3, X4, X5, X6, X7)) → PARSEA_IN_GA(X7)
PARSEA_IN_GA(X1) → U20_GA(X1, appcG_in_aag(X1))
U20_GA(X1, appcG_out_aag(X3, X4, X1)) → U22_GA(X1, appcH_in_gga(X3, X4))
U22_GA(X1, appcH_out_gga(X3, X4, X5)) → PARSEA_IN_GA(X5)
PARSEA_IN_GA(cons(a, cons(s(X1, X2, X3), cons(b, X4)))) → U7_GA(X1, X2, X3, X4, appcB_out_gggga(X1, X2, X3, X4, cons(s(a, s(X1, X2, X3), b), X4)))

The TRS R consists of the following rules:

appcB_in_gggga(X1, X2, X3, X4) → appcB_out_gggga(X1, X2, X3, X4, cons(s(a, s(X1, X2, X3), b), X4))
appcC_in_aaaaag(cons(a, cons(s(X1, X2, X3), cons(b, X4)))) → appcC_out_aaaaag(nil, X1, X2, X3, X4, cons(a, cons(s(X1, X2, X3), cons(b, X4))))
appcC_in_aaaaag(cons(X1, X7)) → U36_aaaaag(X1, X7, appcC_in_aaaaag(X7))
U36_aaaaag(X1, X7, appcC_out_aaaaag(X2, X3, X4, X5, X6, X7)) → appcC_out_aaaaag(cons(X1, X2), X3, X4, X5, X6, cons(X1, X7))
appcD_in_gggggga(X1, X2, X3, X4, X5, X6) → U42_gggggga(X1, X2, X3, X4, X5, X6, appcI_in_ggggga(X2, X3, X4, X5, X6))
appcI_in_ggggga(nil, X1, X2, X3, X4) → appcI_out_ggggga(nil, X1, X2, X3, X4, cons(s(a, s(X1, X2, X3), b), X4))
appcI_in_ggggga(cons(X1, X2), X3, X4, X5, X6) → U37_ggggga(X1, X2, X3, X4, X5, X6, appcI_in_ggggga(X2, X3, X4, X5, X6))
U37_ggggga(X1, X2, X3, X4, X5, X6, appcI_out_ggggga(X2, X3, X4, X5, X6, X7)) → appcI_out_ggggga(cons(X1, X2), X3, X4, X5, X6, cons(X1, X7))
U42_gggggga(X1, X2, X3, X4, X5, X6, appcI_out_ggggga(X2, X3, X4, X5, X6, X7)) → appcD_out_gggggga(X1, X2, X3, X4, X5, X6, cons(X1, X7))
appcE_in_aaaag(cons(a, cons(s(X1, X2), cons(b, X3)))) → appcE_out_aaaag(nil, X1, X2, X3, cons(a, cons(s(X1, X2), cons(b, X3))))
appcE_in_aaaag(cons(X1, X6)) → U38_aaaag(X1, X6, appcE_in_aaaag(X6))
U38_aaaag(X1, X6, appcE_out_aaaag(X2, X3, X4, X5, X6)) → appcE_out_aaaag(cons(X1, X2), X3, X4, X5, cons(X1, X6))
appcF_in_gggga(nil, X1, X2, X3) → appcF_out_gggga(nil, X1, X2, X3, cons(s(a, s(X1, X2), b), X3))
appcF_in_gggga(cons(X1, X2), X3, X4, X5) → U39_gggga(X1, X2, X3, X4, X5, appcF_in_gggga(X2, X3, X4, X5))
U39_gggga(X1, X2, X3, X4, X5, appcF_out_gggga(X2, X3, X4, X5, X6)) → appcF_out_gggga(cons(X1, X2), X3, X4, X5, cons(X1, X6))
appcG_in_aag(cons(a, cons(b, X1))) → appcG_out_aag(nil, X1, cons(a, cons(b, X1)))
appcG_in_aag(cons(X1, X4)) → U40_aag(X1, X4, appcG_in_aag(X4))
U40_aag(X1, X4, appcG_out_aag(X2, X3, X4)) → appcG_out_aag(cons(X1, X2), X3, cons(X1, X4))
appcH_in_gga(nil, X1) → appcH_out_gga(nil, X1, cons(s(a, b), X1))
appcH_in_gga(cons(X1, X2), X3) → U41_gga(X1, X2, X3, appcH_in_gga(X2, X3))
U41_gga(X1, X2, X3, appcH_out_gga(X2, X3, X4)) → appcH_out_gga(cons(X1, X2), X3, cons(X1, X4))

The set Q consists of the following terms:

appcB_in_gggga(x0, x1, x2, x3)
appcC_in_aaaaag(x0)
U36_aaaaag(x0, x1, x2)
appcD_in_gggggga(x0, x1, x2, x3, x4, x5)
appcI_in_ggggga(x0, x1, x2, x3, x4)
U37_ggggga(x0, x1, x2, x3, x4, x5, x6)
U42_gggggga(x0, x1, x2, x3, x4, x5, x6)
appcE_in_aaaag(x0)
U38_aaaag(x0, x1, x2)
appcF_in_gggga(x0, x1, x2, x3)
U39_gggga(x0, x1, x2, x3, x4, x5)
appcG_in_aag(x0)
U40_aag(x0, x1, x2)
appcH_in_gga(x0, x1)
U41_gga(x0, x1, x2, x3)

We have to consider all (P,Q,R)-chains.

(54) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(55) Obligation:

Q DP problem:
The TRS P consists of the following rules:

U7_GA(X1, X2, X3, X4, appcB_out_gggga(X1, X2, X3, X4, X6)) → PARSEA_IN_GA(X6)
PARSEA_IN_GA(cons(X1, X2)) → U10_GA(X1, X2, appcC_in_aaaaag(X2))
U10_GA(X1, X2, appcC_out_aaaaag(X4, X5, X6, X7, X8, X2)) → U12_GA(X1, X2, appcD_in_gggggga(X1, X4, X5, X6, X7, X8))
U12_GA(X1, X2, appcD_out_gggggga(X1, X4, X5, X6, X7, X8, X9)) → PARSEA_IN_GA(X9)
PARSEA_IN_GA(X1) → U15_GA(X1, appcE_in_aaaag(X1))
U15_GA(X1, appcE_out_aaaag(X3, X4, X5, X6, X1)) → U17_GA(X1, appcF_in_gggga(X3, X4, X5, X6))
U17_GA(X1, appcF_out_gggga(X3, X4, X5, X6, X7)) → PARSEA_IN_GA(X7)
PARSEA_IN_GA(X1) → U20_GA(X1, appcG_in_aag(X1))
U20_GA(X1, appcG_out_aag(X3, X4, X1)) → U22_GA(X1, appcH_in_gga(X3, X4))
U22_GA(X1, appcH_out_gga(X3, X4, X5)) → PARSEA_IN_GA(X5)
PARSEA_IN_GA(cons(a, cons(s(X1, X2, X3), cons(b, X4)))) → U7_GA(X1, X2, X3, X4, appcB_out_gggga(X1, X2, X3, X4, cons(s(a, s(X1, X2, X3), b), X4)))

The TRS R consists of the following rules:

appcH_in_gga(nil, X1) → appcH_out_gga(nil, X1, cons(s(a, b), X1))
appcH_in_gga(cons(X1, X2), X3) → U41_gga(X1, X2, X3, appcH_in_gga(X2, X3))
U41_gga(X1, X2, X3, appcH_out_gga(X2, X3, X4)) → appcH_out_gga(cons(X1, X2), X3, cons(X1, X4))
appcG_in_aag(cons(a, cons(b, X1))) → appcG_out_aag(nil, X1, cons(a, cons(b, X1)))
appcG_in_aag(cons(X1, X4)) → U40_aag(X1, X4, appcG_in_aag(X4))
U40_aag(X1, X4, appcG_out_aag(X2, X3, X4)) → appcG_out_aag(cons(X1, X2), X3, cons(X1, X4))
appcF_in_gggga(nil, X1, X2, X3) → appcF_out_gggga(nil, X1, X2, X3, cons(s(a, s(X1, X2), b), X3))
appcF_in_gggga(cons(X1, X2), X3, X4, X5) → U39_gggga(X1, X2, X3, X4, X5, appcF_in_gggga(X2, X3, X4, X5))
U39_gggga(X1, X2, X3, X4, X5, appcF_out_gggga(X2, X3, X4, X5, X6)) → appcF_out_gggga(cons(X1, X2), X3, X4, X5, cons(X1, X6))
appcE_in_aaaag(cons(a, cons(s(X1, X2), cons(b, X3)))) → appcE_out_aaaag(nil, X1, X2, X3, cons(a, cons(s(X1, X2), cons(b, X3))))
appcE_in_aaaag(cons(X1, X6)) → U38_aaaag(X1, X6, appcE_in_aaaag(X6))
U38_aaaag(X1, X6, appcE_out_aaaag(X2, X3, X4, X5, X6)) → appcE_out_aaaag(cons(X1, X2), X3, X4, X5, cons(X1, X6))
appcD_in_gggggga(X1, X2, X3, X4, X5, X6) → U42_gggggga(X1, X2, X3, X4, X5, X6, appcI_in_ggggga(X2, X3, X4, X5, X6))
appcI_in_ggggga(nil, X1, X2, X3, X4) → appcI_out_ggggga(nil, X1, X2, X3, X4, cons(s(a, s(X1, X2, X3), b), X4))
appcI_in_ggggga(cons(X1, X2), X3, X4, X5, X6) → U37_ggggga(X1, X2, X3, X4, X5, X6, appcI_in_ggggga(X2, X3, X4, X5, X6))
U42_gggggga(X1, X2, X3, X4, X5, X6, appcI_out_ggggga(X2, X3, X4, X5, X6, X7)) → appcD_out_gggggga(X1, X2, X3, X4, X5, X6, cons(X1, X7))
U37_ggggga(X1, X2, X3, X4, X5, X6, appcI_out_ggggga(X2, X3, X4, X5, X6, X7)) → appcI_out_ggggga(cons(X1, X2), X3, X4, X5, X6, cons(X1, X7))
appcC_in_aaaaag(cons(a, cons(s(X1, X2, X3), cons(b, X4)))) → appcC_out_aaaaag(nil, X1, X2, X3, X4, cons(a, cons(s(X1, X2, X3), cons(b, X4))))
appcC_in_aaaaag(cons(X1, X7)) → U36_aaaaag(X1, X7, appcC_in_aaaaag(X7))
U36_aaaaag(X1, X7, appcC_out_aaaaag(X2, X3, X4, X5, X6, X7)) → appcC_out_aaaaag(cons(X1, X2), X3, X4, X5, X6, cons(X1, X7))

The set Q consists of the following terms:

appcB_in_gggga(x0, x1, x2, x3)
appcC_in_aaaaag(x0)
U36_aaaaag(x0, x1, x2)
appcD_in_gggggga(x0, x1, x2, x3, x4, x5)
appcI_in_ggggga(x0, x1, x2, x3, x4)
U37_ggggga(x0, x1, x2, x3, x4, x5, x6)
U42_gggggga(x0, x1, x2, x3, x4, x5, x6)
appcE_in_aaaag(x0)
U38_aaaag(x0, x1, x2)
appcF_in_gggga(x0, x1, x2, x3)
U39_gggga(x0, x1, x2, x3, x4, x5)
appcG_in_aag(x0)
U40_aag(x0, x1, x2)
appcH_in_gga(x0, x1)
U41_gga(x0, x1, x2, x3)

We have to consider all (P,Q,R)-chains.

(56) QReductionProof (EQUIVALENT transformation)

We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

appcB_in_gggga(x0, x1, x2, x3)

(57) Obligation:

Q DP problem:
The TRS P consists of the following rules:

U7_GA(X1, X2, X3, X4, appcB_out_gggga(X1, X2, X3, X4, X6)) → PARSEA_IN_GA(X6)
PARSEA_IN_GA(cons(X1, X2)) → U10_GA(X1, X2, appcC_in_aaaaag(X2))
U10_GA(X1, X2, appcC_out_aaaaag(X4, X5, X6, X7, X8, X2)) → U12_GA(X1, X2, appcD_in_gggggga(X1, X4, X5, X6, X7, X8))
U12_GA(X1, X2, appcD_out_gggggga(X1, X4, X5, X6, X7, X8, X9)) → PARSEA_IN_GA(X9)
PARSEA_IN_GA(X1) → U15_GA(X1, appcE_in_aaaag(X1))
U15_GA(X1, appcE_out_aaaag(X3, X4, X5, X6, X1)) → U17_GA(X1, appcF_in_gggga(X3, X4, X5, X6))
U17_GA(X1, appcF_out_gggga(X3, X4, X5, X6, X7)) → PARSEA_IN_GA(X7)
PARSEA_IN_GA(X1) → U20_GA(X1, appcG_in_aag(X1))
U20_GA(X1, appcG_out_aag(X3, X4, X1)) → U22_GA(X1, appcH_in_gga(X3, X4))
U22_GA(X1, appcH_out_gga(X3, X4, X5)) → PARSEA_IN_GA(X5)
PARSEA_IN_GA(cons(a, cons(s(X1, X2, X3), cons(b, X4)))) → U7_GA(X1, X2, X3, X4, appcB_out_gggga(X1, X2, X3, X4, cons(s(a, s(X1, X2, X3), b), X4)))

The TRS R consists of the following rules:

appcH_in_gga(nil, X1) → appcH_out_gga(nil, X1, cons(s(a, b), X1))
appcH_in_gga(cons(X1, X2), X3) → U41_gga(X1, X2, X3, appcH_in_gga(X2, X3))
U41_gga(X1, X2, X3, appcH_out_gga(X2, X3, X4)) → appcH_out_gga(cons(X1, X2), X3, cons(X1, X4))
appcG_in_aag(cons(a, cons(b, X1))) → appcG_out_aag(nil, X1, cons(a, cons(b, X1)))
appcG_in_aag(cons(X1, X4)) → U40_aag(X1, X4, appcG_in_aag(X4))
U40_aag(X1, X4, appcG_out_aag(X2, X3, X4)) → appcG_out_aag(cons(X1, X2), X3, cons(X1, X4))
appcF_in_gggga(nil, X1, X2, X3) → appcF_out_gggga(nil, X1, X2, X3, cons(s(a, s(X1, X2), b), X3))
appcF_in_gggga(cons(X1, X2), X3, X4, X5) → U39_gggga(X1, X2, X3, X4, X5, appcF_in_gggga(X2, X3, X4, X5))
U39_gggga(X1, X2, X3, X4, X5, appcF_out_gggga(X2, X3, X4, X5, X6)) → appcF_out_gggga(cons(X1, X2), X3, X4, X5, cons(X1, X6))
appcE_in_aaaag(cons(a, cons(s(X1, X2), cons(b, X3)))) → appcE_out_aaaag(nil, X1, X2, X3, cons(a, cons(s(X1, X2), cons(b, X3))))
appcE_in_aaaag(cons(X1, X6)) → U38_aaaag(X1, X6, appcE_in_aaaag(X6))
U38_aaaag(X1, X6, appcE_out_aaaag(X2, X3, X4, X5, X6)) → appcE_out_aaaag(cons(X1, X2), X3, X4, X5, cons(X1, X6))
appcD_in_gggggga(X1, X2, X3, X4, X5, X6) → U42_gggggga(X1, X2, X3, X4, X5, X6, appcI_in_ggggga(X2, X3, X4, X5, X6))
appcI_in_ggggga(nil, X1, X2, X3, X4) → appcI_out_ggggga(nil, X1, X2, X3, X4, cons(s(a, s(X1, X2, X3), b), X4))
appcI_in_ggggga(cons(X1, X2), X3, X4, X5, X6) → U37_ggggga(X1, X2, X3, X4, X5, X6, appcI_in_ggggga(X2, X3, X4, X5, X6))
U42_gggggga(X1, X2, X3, X4, X5, X6, appcI_out_ggggga(X2, X3, X4, X5, X6, X7)) → appcD_out_gggggga(X1, X2, X3, X4, X5, X6, cons(X1, X7))
U37_ggggga(X1, X2, X3, X4, X5, X6, appcI_out_ggggga(X2, X3, X4, X5, X6, X7)) → appcI_out_ggggga(cons(X1, X2), X3, X4, X5, X6, cons(X1, X7))
appcC_in_aaaaag(cons(a, cons(s(X1, X2, X3), cons(b, X4)))) → appcC_out_aaaaag(nil, X1, X2, X3, X4, cons(a, cons(s(X1, X2, X3), cons(b, X4))))
appcC_in_aaaaag(cons(X1, X7)) → U36_aaaaag(X1, X7, appcC_in_aaaaag(X7))
U36_aaaaag(X1, X7, appcC_out_aaaaag(X2, X3, X4, X5, X6, X7)) → appcC_out_aaaaag(cons(X1, X2), X3, X4, X5, X6, cons(X1, X7))

The set Q consists of the following terms:

appcC_in_aaaaag(x0)
U36_aaaaag(x0, x1, x2)
appcD_in_gggggga(x0, x1, x2, x3, x4, x5)
appcI_in_ggggga(x0, x1, x2, x3, x4)
U37_ggggga(x0, x1, x2, x3, x4, x5, x6)
U42_gggggga(x0, x1, x2, x3, x4, x5, x6)
appcE_in_aaaag(x0)
U38_aaaag(x0, x1, x2)
appcF_in_gggga(x0, x1, x2, x3)
U39_gggga(x0, x1, x2, x3, x4, x5)
appcG_in_aag(x0)
U40_aag(x0, x1, x2)
appcH_in_gga(x0, x1)
U41_gga(x0, x1, x2, x3)

We have to consider all (P,Q,R)-chains.

(58) Rewriting (EQUIVALENT transformation)

By rewriting [LPAR04] the rule U10_GA(X1, X2, appcC_out_aaaaag(X4, X5, X6, X7, X8, X2)) → U12_GA(X1, X2, appcD_in_gggggga(X1, X4, X5, X6, X7, X8)) at position [2] we obtained the following new rules [LPAR04]:

U10_GA(X1, X2, appcC_out_aaaaag(X4, X5, X6, X7, X8, X2)) → U12_GA(X1, X2, U42_gggggga(X1, X4, X5, X6, X7, X8, appcI_in_ggggga(X4, X5, X6, X7, X8)))

(59) Obligation:

Q DP problem:
The TRS P consists of the following rules:

U7_GA(X1, X2, X3, X4, appcB_out_gggga(X1, X2, X3, X4, X6)) → PARSEA_IN_GA(X6)
PARSEA_IN_GA(cons(X1, X2)) → U10_GA(X1, X2, appcC_in_aaaaag(X2))
U12_GA(X1, X2, appcD_out_gggggga(X1, X4, X5, X6, X7, X8, X9)) → PARSEA_IN_GA(X9)
PARSEA_IN_GA(X1) → U15_GA(X1, appcE_in_aaaag(X1))
U15_GA(X1, appcE_out_aaaag(X3, X4, X5, X6, X1)) → U17_GA(X1, appcF_in_gggga(X3, X4, X5, X6))
U17_GA(X1, appcF_out_gggga(X3, X4, X5, X6, X7)) → PARSEA_IN_GA(X7)
PARSEA_IN_GA(X1) → U20_GA(X1, appcG_in_aag(X1))
U20_GA(X1, appcG_out_aag(X3, X4, X1)) → U22_GA(X1, appcH_in_gga(X3, X4))
U22_GA(X1, appcH_out_gga(X3, X4, X5)) → PARSEA_IN_GA(X5)
PARSEA_IN_GA(cons(a, cons(s(X1, X2, X3), cons(b, X4)))) → U7_GA(X1, X2, X3, X4, appcB_out_gggga(X1, X2, X3, X4, cons(s(a, s(X1, X2, X3), b), X4)))
U10_GA(X1, X2, appcC_out_aaaaag(X4, X5, X6, X7, X8, X2)) → U12_GA(X1, X2, U42_gggggga(X1, X4, X5, X6, X7, X8, appcI_in_ggggga(X4, X5, X6, X7, X8)))

The TRS R consists of the following rules:

appcH_in_gga(nil, X1) → appcH_out_gga(nil, X1, cons(s(a, b), X1))
appcH_in_gga(cons(X1, X2), X3) → U41_gga(X1, X2, X3, appcH_in_gga(X2, X3))
U41_gga(X1, X2, X3, appcH_out_gga(X2, X3, X4)) → appcH_out_gga(cons(X1, X2), X3, cons(X1, X4))
appcG_in_aag(cons(a, cons(b, X1))) → appcG_out_aag(nil, X1, cons(a, cons(b, X1)))
appcG_in_aag(cons(X1, X4)) → U40_aag(X1, X4, appcG_in_aag(X4))
U40_aag(X1, X4, appcG_out_aag(X2, X3, X4)) → appcG_out_aag(cons(X1, X2), X3, cons(X1, X4))
appcF_in_gggga(nil, X1, X2, X3) → appcF_out_gggga(nil, X1, X2, X3, cons(s(a, s(X1, X2), b), X3))
appcF_in_gggga(cons(X1, X2), X3, X4, X5) → U39_gggga(X1, X2, X3, X4, X5, appcF_in_gggga(X2, X3, X4, X5))
U39_gggga(X1, X2, X3, X4, X5, appcF_out_gggga(X2, X3, X4, X5, X6)) → appcF_out_gggga(cons(X1, X2), X3, X4, X5, cons(X1, X6))
appcE_in_aaaag(cons(a, cons(s(X1, X2), cons(b, X3)))) → appcE_out_aaaag(nil, X1, X2, X3, cons(a, cons(s(X1, X2), cons(b, X3))))
appcE_in_aaaag(cons(X1, X6)) → U38_aaaag(X1, X6, appcE_in_aaaag(X6))
U38_aaaag(X1, X6, appcE_out_aaaag(X2, X3, X4, X5, X6)) → appcE_out_aaaag(cons(X1, X2), X3, X4, X5, cons(X1, X6))
appcD_in_gggggga(X1, X2, X3, X4, X5, X6) → U42_gggggga(X1, X2, X3, X4, X5, X6, appcI_in_ggggga(X2, X3, X4, X5, X6))
appcI_in_ggggga(nil, X1, X2, X3, X4) → appcI_out_ggggga(nil, X1, X2, X3, X4, cons(s(a, s(X1, X2, X3), b), X4))
appcI_in_ggggga(cons(X1, X2), X3, X4, X5, X6) → U37_ggggga(X1, X2, X3, X4, X5, X6, appcI_in_ggggga(X2, X3, X4, X5, X6))
U42_gggggga(X1, X2, X3, X4, X5, X6, appcI_out_ggggga(X2, X3, X4, X5, X6, X7)) → appcD_out_gggggga(X1, X2, X3, X4, X5, X6, cons(X1, X7))
U37_ggggga(X1, X2, X3, X4, X5, X6, appcI_out_ggggga(X2, X3, X4, X5, X6, X7)) → appcI_out_ggggga(cons(X1, X2), X3, X4, X5, X6, cons(X1, X7))
appcC_in_aaaaag(cons(a, cons(s(X1, X2, X3), cons(b, X4)))) → appcC_out_aaaaag(nil, X1, X2, X3, X4, cons(a, cons(s(X1, X2, X3), cons(b, X4))))
appcC_in_aaaaag(cons(X1, X7)) → U36_aaaaag(X1, X7, appcC_in_aaaaag(X7))
U36_aaaaag(X1, X7, appcC_out_aaaaag(X2, X3, X4, X5, X6, X7)) → appcC_out_aaaaag(cons(X1, X2), X3, X4, X5, X6, cons(X1, X7))

The set Q consists of the following terms:

appcC_in_aaaaag(x0)
U36_aaaaag(x0, x1, x2)
appcD_in_gggggga(x0, x1, x2, x3, x4, x5)
appcI_in_ggggga(x0, x1, x2, x3, x4)
U37_ggggga(x0, x1, x2, x3, x4, x5, x6)
U42_gggggga(x0, x1, x2, x3, x4, x5, x6)
appcE_in_aaaag(x0)
U38_aaaag(x0, x1, x2)
appcF_in_gggga(x0, x1, x2, x3)
U39_gggga(x0, x1, x2, x3, x4, x5)
appcG_in_aag(x0)
U40_aag(x0, x1, x2)
appcH_in_gga(x0, x1)
U41_gga(x0, x1, x2, x3)

We have to consider all (P,Q,R)-chains.

(60) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(61) Obligation:

Q DP problem:
The TRS P consists of the following rules:

U7_GA(X1, X2, X3, X4, appcB_out_gggga(X1, X2, X3, X4, X6)) → PARSEA_IN_GA(X6)
PARSEA_IN_GA(cons(X1, X2)) → U10_GA(X1, X2, appcC_in_aaaaag(X2))
U12_GA(X1, X2, appcD_out_gggggga(X1, X4, X5, X6, X7, X8, X9)) → PARSEA_IN_GA(X9)
PARSEA_IN_GA(X1) → U15_GA(X1, appcE_in_aaaag(X1))
U15_GA(X1, appcE_out_aaaag(X3, X4, X5, X6, X1)) → U17_GA(X1, appcF_in_gggga(X3, X4, X5, X6))
U17_GA(X1, appcF_out_gggga(X3, X4, X5, X6, X7)) → PARSEA_IN_GA(X7)
PARSEA_IN_GA(X1) → U20_GA(X1, appcG_in_aag(X1))
U20_GA(X1, appcG_out_aag(X3, X4, X1)) → U22_GA(X1, appcH_in_gga(X3, X4))
U22_GA(X1, appcH_out_gga(X3, X4, X5)) → PARSEA_IN_GA(X5)
PARSEA_IN_GA(cons(a, cons(s(X1, X2, X3), cons(b, X4)))) → U7_GA(X1, X2, X3, X4, appcB_out_gggga(X1, X2, X3, X4, cons(s(a, s(X1, X2, X3), b), X4)))
U10_GA(X1, X2, appcC_out_aaaaag(X4, X5, X6, X7, X8, X2)) → U12_GA(X1, X2, U42_gggggga(X1, X4, X5, X6, X7, X8, appcI_in_ggggga(X4, X5, X6, X7, X8)))

The TRS R consists of the following rules:

appcI_in_ggggga(nil, X1, X2, X3, X4) → appcI_out_ggggga(nil, X1, X2, X3, X4, cons(s(a, s(X1, X2, X3), b), X4))
appcI_in_ggggga(cons(X1, X2), X3, X4, X5, X6) → U37_ggggga(X1, X2, X3, X4, X5, X6, appcI_in_ggggga(X2, X3, X4, X5, X6))
U42_gggggga(X1, X2, X3, X4, X5, X6, appcI_out_ggggga(X2, X3, X4, X5, X6, X7)) → appcD_out_gggggga(X1, X2, X3, X4, X5, X6, cons(X1, X7))
U37_ggggga(X1, X2, X3, X4, X5, X6, appcI_out_ggggga(X2, X3, X4, X5, X6, X7)) → appcI_out_ggggga(cons(X1, X2), X3, X4, X5, X6, cons(X1, X7))
appcH_in_gga(nil, X1) → appcH_out_gga(nil, X1, cons(s(a, b), X1))
appcH_in_gga(cons(X1, X2), X3) → U41_gga(X1, X2, X3, appcH_in_gga(X2, X3))
U41_gga(X1, X2, X3, appcH_out_gga(X2, X3, X4)) → appcH_out_gga(cons(X1, X2), X3, cons(X1, X4))
appcG_in_aag(cons(a, cons(b, X1))) → appcG_out_aag(nil, X1, cons(a, cons(b, X1)))
appcG_in_aag(cons(X1, X4)) → U40_aag(X1, X4, appcG_in_aag(X4))
U40_aag(X1, X4, appcG_out_aag(X2, X3, X4)) → appcG_out_aag(cons(X1, X2), X3, cons(X1, X4))
appcF_in_gggga(nil, X1, X2, X3) → appcF_out_gggga(nil, X1, X2, X3, cons(s(a, s(X1, X2), b), X3))
appcF_in_gggga(cons(X1, X2), X3, X4, X5) → U39_gggga(X1, X2, X3, X4, X5, appcF_in_gggga(X2, X3, X4, X5))
U39_gggga(X1, X2, X3, X4, X5, appcF_out_gggga(X2, X3, X4, X5, X6)) → appcF_out_gggga(cons(X1, X2), X3, X4, X5, cons(X1, X6))
appcE_in_aaaag(cons(a, cons(s(X1, X2), cons(b, X3)))) → appcE_out_aaaag(nil, X1, X2, X3, cons(a, cons(s(X1, X2), cons(b, X3))))
appcE_in_aaaag(cons(X1, X6)) → U38_aaaag(X1, X6, appcE_in_aaaag(X6))
U38_aaaag(X1, X6, appcE_out_aaaag(X2, X3, X4, X5, X6)) → appcE_out_aaaag(cons(X1, X2), X3, X4, X5, cons(X1, X6))
appcC_in_aaaaag(cons(a, cons(s(X1, X2, X3), cons(b, X4)))) → appcC_out_aaaaag(nil, X1, X2, X3, X4, cons(a, cons(s(X1, X2, X3), cons(b, X4))))
appcC_in_aaaaag(cons(X1, X7)) → U36_aaaaag(X1, X7, appcC_in_aaaaag(X7))
U36_aaaaag(X1, X7, appcC_out_aaaaag(X2, X3, X4, X5, X6, X7)) → appcC_out_aaaaag(cons(X1, X2), X3, X4, X5, X6, cons(X1, X7))

The set Q consists of the following terms:

appcC_in_aaaaag(x0)
U36_aaaaag(x0, x1, x2)
appcD_in_gggggga(x0, x1, x2, x3, x4, x5)
appcI_in_ggggga(x0, x1, x2, x3, x4)
U37_ggggga(x0, x1, x2, x3, x4, x5, x6)
U42_gggggga(x0, x1, x2, x3, x4, x5, x6)
appcE_in_aaaag(x0)
U38_aaaag(x0, x1, x2)
appcF_in_gggga(x0, x1, x2, x3)
U39_gggga(x0, x1, x2, x3, x4, x5)
appcG_in_aag(x0)
U40_aag(x0, x1, x2)
appcH_in_gga(x0, x1)
U41_gga(x0, x1, x2, x3)

We have to consider all (P,Q,R)-chains.

(62) QReductionProof (EQUIVALENT transformation)

We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

appcD_in_gggggga(x0, x1, x2, x3, x4, x5)

(63) Obligation:

Q DP problem:
The TRS P consists of the following rules:

U7_GA(X1, X2, X3, X4, appcB_out_gggga(X1, X2, X3, X4, X6)) → PARSEA_IN_GA(X6)
PARSEA_IN_GA(cons(X1, X2)) → U10_GA(X1, X2, appcC_in_aaaaag(X2))
U12_GA(X1, X2, appcD_out_gggggga(X1, X4, X5, X6, X7, X8, X9)) → PARSEA_IN_GA(X9)
PARSEA_IN_GA(X1) → U15_GA(X1, appcE_in_aaaag(X1))
U15_GA(X1, appcE_out_aaaag(X3, X4, X5, X6, X1)) → U17_GA(X1, appcF_in_gggga(X3, X4, X5, X6))
U17_GA(X1, appcF_out_gggga(X3, X4, X5, X6, X7)) → PARSEA_IN_GA(X7)
PARSEA_IN_GA(X1) → U20_GA(X1, appcG_in_aag(X1))
U20_GA(X1, appcG_out_aag(X3, X4, X1)) → U22_GA(X1, appcH_in_gga(X3, X4))
U22_GA(X1, appcH_out_gga(X3, X4, X5)) → PARSEA_IN_GA(X5)
PARSEA_IN_GA(cons(a, cons(s(X1, X2, X3), cons(b, X4)))) → U7_GA(X1, X2, X3, X4, appcB_out_gggga(X1, X2, X3, X4, cons(s(a, s(X1, X2, X3), b), X4)))
U10_GA(X1, X2, appcC_out_aaaaag(X4, X5, X6, X7, X8, X2)) → U12_GA(X1, X2, U42_gggggga(X1, X4, X5, X6, X7, X8, appcI_in_ggggga(X4, X5, X6, X7, X8)))

The TRS R consists of the following rules:

appcI_in_ggggga(nil, X1, X2, X3, X4) → appcI_out_ggggga(nil, X1, X2, X3, X4, cons(s(a, s(X1, X2, X3), b), X4))
appcI_in_ggggga(cons(X1, X2), X3, X4, X5, X6) → U37_ggggga(X1, X2, X3, X4, X5, X6, appcI_in_ggggga(X2, X3, X4, X5, X6))
U42_gggggga(X1, X2, X3, X4, X5, X6, appcI_out_ggggga(X2, X3, X4, X5, X6, X7)) → appcD_out_gggggga(X1, X2, X3, X4, X5, X6, cons(X1, X7))
U37_ggggga(X1, X2, X3, X4, X5, X6, appcI_out_ggggga(X2, X3, X4, X5, X6, X7)) → appcI_out_ggggga(cons(X1, X2), X3, X4, X5, X6, cons(X1, X7))
appcH_in_gga(nil, X1) → appcH_out_gga(nil, X1, cons(s(a, b), X1))
appcH_in_gga(cons(X1, X2), X3) → U41_gga(X1, X2, X3, appcH_in_gga(X2, X3))
U41_gga(X1, X2, X3, appcH_out_gga(X2, X3, X4)) → appcH_out_gga(cons(X1, X2), X3, cons(X1, X4))
appcG_in_aag(cons(a, cons(b, X1))) → appcG_out_aag(nil, X1, cons(a, cons(b, X1)))
appcG_in_aag(cons(X1, X4)) → U40_aag(X1, X4, appcG_in_aag(X4))
U40_aag(X1, X4, appcG_out_aag(X2, X3, X4)) → appcG_out_aag(cons(X1, X2), X3, cons(X1, X4))
appcF_in_gggga(nil, X1, X2, X3) → appcF_out_gggga(nil, X1, X2, X3, cons(s(a, s(X1, X2), b), X3))
appcF_in_gggga(cons(X1, X2), X3, X4, X5) → U39_gggga(X1, X2, X3, X4, X5, appcF_in_gggga(X2, X3, X4, X5))
U39_gggga(X1, X2, X3, X4, X5, appcF_out_gggga(X2, X3, X4, X5, X6)) → appcF_out_gggga(cons(X1, X2), X3, X4, X5, cons(X1, X6))
appcE_in_aaaag(cons(a, cons(s(X1, X2), cons(b, X3)))) → appcE_out_aaaag(nil, X1, X2, X3, cons(a, cons(s(X1, X2), cons(b, X3))))
appcE_in_aaaag(cons(X1, X6)) → U38_aaaag(X1, X6, appcE_in_aaaag(X6))
U38_aaaag(X1, X6, appcE_out_aaaag(X2, X3, X4, X5, X6)) → appcE_out_aaaag(cons(X1, X2), X3, X4, X5, cons(X1, X6))
appcC_in_aaaaag(cons(a, cons(s(X1, X2, X3), cons(b, X4)))) → appcC_out_aaaaag(nil, X1, X2, X3, X4, cons(a, cons(s(X1, X2, X3), cons(b, X4))))
appcC_in_aaaaag(cons(X1, X7)) → U36_aaaaag(X1, X7, appcC_in_aaaaag(X7))
U36_aaaaag(X1, X7, appcC_out_aaaaag(X2, X3, X4, X5, X6, X7)) → appcC_out_aaaaag(cons(X1, X2), X3, X4, X5, X6, cons(X1, X7))

The set Q consists of the following terms:

appcC_in_aaaaag(x0)
U36_aaaaag(x0, x1, x2)
appcI_in_ggggga(x0, x1, x2, x3, x4)
U37_ggggga(x0, x1, x2, x3, x4, x5, x6)
U42_gggggga(x0, x1, x2, x3, x4, x5, x6)
appcE_in_aaaag(x0)
U38_aaaag(x0, x1, x2)
appcF_in_gggga(x0, x1, x2, x3)
U39_gggga(x0, x1, x2, x3, x4, x5)
appcG_in_aag(x0)
U40_aag(x0, x1, x2)
appcH_in_gga(x0, x1)
U41_gga(x0, x1, x2, x3)

We have to consider all (P,Q,R)-chains.

(64) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule U7_GA(X1, X2, X3, X4, appcB_out_gggga(X1, X2, X3, X4, X6)) → PARSEA_IN_GA(X6) we obtained the following new rules [LPAR04]:

U7_GA(z0, z1, z2, z3, appcB_out_gggga(z0, z1, z2, z3, cons(s(a, s(z0, z1, z2), b), z3))) → PARSEA_IN_GA(cons(s(a, s(z0, z1, z2), b), z3))

(65) Obligation:

Q DP problem:
The TRS P consists of the following rules:

PARSEA_IN_GA(cons(X1, X2)) → U10_GA(X1, X2, appcC_in_aaaaag(X2))
U12_GA(X1, X2, appcD_out_gggggga(X1, X4, X5, X6, X7, X8, X9)) → PARSEA_IN_GA(X9)
PARSEA_IN_GA(X1) → U15_GA(X1, appcE_in_aaaag(X1))
U15_GA(X1, appcE_out_aaaag(X3, X4, X5, X6, X1)) → U17_GA(X1, appcF_in_gggga(X3, X4, X5, X6))
U17_GA(X1, appcF_out_gggga(X3, X4, X5, X6, X7)) → PARSEA_IN_GA(X7)
PARSEA_IN_GA(X1) → U20_GA(X1, appcG_in_aag(X1))
U20_GA(X1, appcG_out_aag(X3, X4, X1)) → U22_GA(X1, appcH_in_gga(X3, X4))
U22_GA(X1, appcH_out_gga(X3, X4, X5)) → PARSEA_IN_GA(X5)
PARSEA_IN_GA(cons(a, cons(s(X1, X2, X3), cons(b, X4)))) → U7_GA(X1, X2, X3, X4, appcB_out_gggga(X1, X2, X3, X4, cons(s(a, s(X1, X2, X3), b), X4)))
U10_GA(X1, X2, appcC_out_aaaaag(X4, X5, X6, X7, X8, X2)) → U12_GA(X1, X2, U42_gggggga(X1, X4, X5, X6, X7, X8, appcI_in_ggggga(X4, X5, X6, X7, X8)))
U7_GA(z0, z1, z2, z3, appcB_out_gggga(z0, z1, z2, z3, cons(s(a, s(z0, z1, z2), b), z3))) → PARSEA_IN_GA(cons(s(a, s(z0, z1, z2), b), z3))

The TRS R consists of the following rules:

appcI_in_ggggga(nil, X1, X2, X3, X4) → appcI_out_ggggga(nil, X1, X2, X3, X4, cons(s(a, s(X1, X2, X3), b), X4))
appcI_in_ggggga(cons(X1, X2), X3, X4, X5, X6) → U37_ggggga(X1, X2, X3, X4, X5, X6, appcI_in_ggggga(X2, X3, X4, X5, X6))
U42_gggggga(X1, X2, X3, X4, X5, X6, appcI_out_ggggga(X2, X3, X4, X5, X6, X7)) → appcD_out_gggggga(X1, X2, X3, X4, X5, X6, cons(X1, X7))
U37_ggggga(X1, X2, X3, X4, X5, X6, appcI_out_ggggga(X2, X3, X4, X5, X6, X7)) → appcI_out_ggggga(cons(X1, X2), X3, X4, X5, X6, cons(X1, X7))
appcH_in_gga(nil, X1) → appcH_out_gga(nil, X1, cons(s(a, b), X1))
appcH_in_gga(cons(X1, X2), X3) → U41_gga(X1, X2, X3, appcH_in_gga(X2, X3))
U41_gga(X1, X2, X3, appcH_out_gga(X2, X3, X4)) → appcH_out_gga(cons(X1, X2), X3, cons(X1, X4))
appcG_in_aag(cons(a, cons(b, X1))) → appcG_out_aag(nil, X1, cons(a, cons(b, X1)))
appcG_in_aag(cons(X1, X4)) → U40_aag(X1, X4, appcG_in_aag(X4))
U40_aag(X1, X4, appcG_out_aag(X2, X3, X4)) → appcG_out_aag(cons(X1, X2), X3, cons(X1, X4))
appcF_in_gggga(nil, X1, X2, X3) → appcF_out_gggga(nil, X1, X2, X3, cons(s(a, s(X1, X2), b), X3))
appcF_in_gggga(cons(X1, X2), X3, X4, X5) → U39_gggga(X1, X2, X3, X4, X5, appcF_in_gggga(X2, X3, X4, X5))
U39_gggga(X1, X2, X3, X4, X5, appcF_out_gggga(X2, X3, X4, X5, X6)) → appcF_out_gggga(cons(X1, X2), X3, X4, X5, cons(X1, X6))
appcE_in_aaaag(cons(a, cons(s(X1, X2), cons(b, X3)))) → appcE_out_aaaag(nil, X1, X2, X3, cons(a, cons(s(X1, X2), cons(b, X3))))
appcE_in_aaaag(cons(X1, X6)) → U38_aaaag(X1, X6, appcE_in_aaaag(X6))
U38_aaaag(X1, X6, appcE_out_aaaag(X2, X3, X4, X5, X6)) → appcE_out_aaaag(cons(X1, X2), X3, X4, X5, cons(X1, X6))
appcC_in_aaaaag(cons(a, cons(s(X1, X2, X3), cons(b, X4)))) → appcC_out_aaaaag(nil, X1, X2, X3, X4, cons(a, cons(s(X1, X2, X3), cons(b, X4))))
appcC_in_aaaaag(cons(X1, X7)) → U36_aaaaag(X1, X7, appcC_in_aaaaag(X7))
U36_aaaaag(X1, X7, appcC_out_aaaaag(X2, X3, X4, X5, X6, X7)) → appcC_out_aaaaag(cons(X1, X2), X3, X4, X5, X6, cons(X1, X7))

The set Q consists of the following terms:

appcC_in_aaaaag(x0)
U36_aaaaag(x0, x1, x2)
appcI_in_ggggga(x0, x1, x2, x3, x4)
U37_ggggga(x0, x1, x2, x3, x4, x5, x6)
U42_gggggga(x0, x1, x2, x3, x4, x5, x6)
appcE_in_aaaag(x0)
U38_aaaag(x0, x1, x2)
appcF_in_gggga(x0, x1, x2, x3)
U39_gggga(x0, x1, x2, x3, x4, x5)
appcG_in_aag(x0)
U40_aag(x0, x1, x2)
appcH_in_gga(x0, x1)
U41_gga(x0, x1, x2, x3)

We have to consider all (P,Q,R)-chains.

(66) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04,JAR06].


The following pairs can be oriented strictly and are deleted.


PARSEA_IN_GA(cons(X1, X2)) → U10_GA(X1, X2, appcC_in_aaaaag(X2))
U15_GA(X1, appcE_out_aaaag(X3, X4, X5, X6, X1)) → U17_GA(X1, appcF_in_gggga(X3, X4, X5, X6))
PARSEA_IN_GA(cons(a, cons(s(X1, X2, X3), cons(b, X4)))) → U7_GA(X1, X2, X3, X4, appcB_out_gggga(X1, X2, X3, X4, cons(s(a, s(X1, X2, X3), b), X4)))
U7_GA(z0, z1, z2, z3, appcB_out_gggga(z0, z1, z2, z3, cons(s(a, s(z0, z1, z2), b), z3))) → PARSEA_IN_GA(cons(s(a, s(z0, z1, z2), b), z3))
The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial interpretation [POLO]:

POL(PARSEA_IN_GA(x1)) = x1   
POL(U10_GA(x1, x2, x3)) = x3   
POL(U12_GA(x1, x2, x3)) = x3   
POL(U15_GA(x1, x2)) = x2   
POL(U17_GA(x1, x2)) = x2   
POL(U20_GA(x1, x2)) = x2   
POL(U22_GA(x1, x2)) = x2   
POL(U36_aaaaag(x1, x2, x3)) = 1 + x3   
POL(U37_ggggga(x1, x2, x3, x4, x5, x6, x7)) = 1 + x7   
POL(U38_aaaag(x1, x2, x3)) = 1 + x3   
POL(U39_gggga(x1, x2, x3, x4, x5, x6)) = 1 + x6   
POL(U40_aag(x1, x2, x3)) = 1 + x3   
POL(U41_gga(x1, x2, x3, x4)) = 1 + x4   
POL(U42_gggggga(x1, x2, x3, x4, x5, x6, x7)) = 1 + x7   
POL(U7_GA(x1, x2, x3, x4, x5)) = 1 + x5   
POL(a) = 0   
POL(appcB_out_gggga(x1, x2, x3, x4, x5)) = x5   
POL(appcC_in_aaaaag(x1)) = x1   
POL(appcC_out_aaaaag(x1, x2, x3, x4, x5, x6)) = 1 + x1 + x5   
POL(appcD_out_gggggga(x1, x2, x3, x4, x5, x6, x7)) = x7   
POL(appcE_in_aaaag(x1)) = x1   
POL(appcE_out_aaaag(x1, x2, x3, x4, x5)) = 1 + x1 + x4   
POL(appcF_in_gggga(x1, x2, x3, x4)) = x1 + x4   
POL(appcF_out_gggga(x1, x2, x3, x4, x5)) = x5   
POL(appcG_in_aag(x1)) = x1   
POL(appcG_out_aag(x1, x2, x3)) = x1 + x2   
POL(appcH_in_gga(x1, x2)) = x1 + x2   
POL(appcH_out_gga(x1, x2, x3)) = x3   
POL(appcI_in_ggggga(x1, x2, x3, x4, x5)) = x1 + x5   
POL(appcI_out_ggggga(x1, x2, x3, x4, x5, x6)) = x6   
POL(b) = 0   
POL(cons(x1, x2)) = 1 + x2   
POL(nil) = 1   
POL(s(x1, x2)) = 0   
POL(s(x1, x2, x3)) = 0   

The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:

appcC_in_aaaaag(cons(a, cons(s(X1, X2, X3), cons(b, X4)))) → appcC_out_aaaaag(nil, X1, X2, X3, X4, cons(a, cons(s(X1, X2, X3), cons(b, X4))))
appcC_in_aaaaag(cons(X1, X7)) → U36_aaaaag(X1, X7, appcC_in_aaaaag(X7))
appcE_in_aaaag(cons(a, cons(s(X1, X2), cons(b, X3)))) → appcE_out_aaaag(nil, X1, X2, X3, cons(a, cons(s(X1, X2), cons(b, X3))))
appcE_in_aaaag(cons(X1, X6)) → U38_aaaag(X1, X6, appcE_in_aaaag(X6))
appcF_in_gggga(nil, X1, X2, X3) → appcF_out_gggga(nil, X1, X2, X3, cons(s(a, s(X1, X2), b), X3))
appcF_in_gggga(cons(X1, X2), X3, X4, X5) → U39_gggga(X1, X2, X3, X4, X5, appcF_in_gggga(X2, X3, X4, X5))
appcG_in_aag(cons(a, cons(b, X1))) → appcG_out_aag(nil, X1, cons(a, cons(b, X1)))
appcG_in_aag(cons(X1, X4)) → U40_aag(X1, X4, appcG_in_aag(X4))
appcH_in_gga(nil, X1) → appcH_out_gga(nil, X1, cons(s(a, b), X1))
appcH_in_gga(cons(X1, X2), X3) → U41_gga(X1, X2, X3, appcH_in_gga(X2, X3))
appcI_in_ggggga(nil, X1, X2, X3, X4) → appcI_out_ggggga(nil, X1, X2, X3, X4, cons(s(a, s(X1, X2, X3), b), X4))
appcI_in_ggggga(cons(X1, X2), X3, X4, X5, X6) → U37_ggggga(X1, X2, X3, X4, X5, X6, appcI_in_ggggga(X2, X3, X4, X5, X6))
U42_gggggga(X1, X2, X3, X4, X5, X6, appcI_out_ggggga(X2, X3, X4, X5, X6, X7)) → appcD_out_gggggga(X1, X2, X3, X4, X5, X6, cons(X1, X7))
U37_ggggga(X1, X2, X3, X4, X5, X6, appcI_out_ggggga(X2, X3, X4, X5, X6, X7)) → appcI_out_ggggga(cons(X1, X2), X3, X4, X5, X6, cons(X1, X7))
U41_gga(X1, X2, X3, appcH_out_gga(X2, X3, X4)) → appcH_out_gga(cons(X1, X2), X3, cons(X1, X4))
U40_aag(X1, X4, appcG_out_aag(X2, X3, X4)) → appcG_out_aag(cons(X1, X2), X3, cons(X1, X4))
U39_gggga(X1, X2, X3, X4, X5, appcF_out_gggga(X2, X3, X4, X5, X6)) → appcF_out_gggga(cons(X1, X2), X3, X4, X5, cons(X1, X6))
U38_aaaag(X1, X6, appcE_out_aaaag(X2, X3, X4, X5, X6)) → appcE_out_aaaag(cons(X1, X2), X3, X4, X5, cons(X1, X6))
U36_aaaaag(X1, X7, appcC_out_aaaaag(X2, X3, X4, X5, X6, X7)) → appcC_out_aaaaag(cons(X1, X2), X3, X4, X5, X6, cons(X1, X7))

(67) Obligation:

Q DP problem:
The TRS P consists of the following rules:

U12_GA(X1, X2, appcD_out_gggggga(X1, X4, X5, X6, X7, X8, X9)) → PARSEA_IN_GA(X9)
PARSEA_IN_GA(X1) → U15_GA(X1, appcE_in_aaaag(X1))
U17_GA(X1, appcF_out_gggga(X3, X4, X5, X6, X7)) → PARSEA_IN_GA(X7)
PARSEA_IN_GA(X1) → U20_GA(X1, appcG_in_aag(X1))
U20_GA(X1, appcG_out_aag(X3, X4, X1)) → U22_GA(X1, appcH_in_gga(X3, X4))
U22_GA(X1, appcH_out_gga(X3, X4, X5)) → PARSEA_IN_GA(X5)
U10_GA(X1, X2, appcC_out_aaaaag(X4, X5, X6, X7, X8, X2)) → U12_GA(X1, X2, U42_gggggga(X1, X4, X5, X6, X7, X8, appcI_in_ggggga(X4, X5, X6, X7, X8)))

The TRS R consists of the following rules:

appcI_in_ggggga(nil, X1, X2, X3, X4) → appcI_out_ggggga(nil, X1, X2, X3, X4, cons(s(a, s(X1, X2, X3), b), X4))
appcI_in_ggggga(cons(X1, X2), X3, X4, X5, X6) → U37_ggggga(X1, X2, X3, X4, X5, X6, appcI_in_ggggga(X2, X3, X4, X5, X6))
U42_gggggga(X1, X2, X3, X4, X5, X6, appcI_out_ggggga(X2, X3, X4, X5, X6, X7)) → appcD_out_gggggga(X1, X2, X3, X4, X5, X6, cons(X1, X7))
U37_ggggga(X1, X2, X3, X4, X5, X6, appcI_out_ggggga(X2, X3, X4, X5, X6, X7)) → appcI_out_ggggga(cons(X1, X2), X3, X4, X5, X6, cons(X1, X7))
appcH_in_gga(nil, X1) → appcH_out_gga(nil, X1, cons(s(a, b), X1))
appcH_in_gga(cons(X1, X2), X3) → U41_gga(X1, X2, X3, appcH_in_gga(X2, X3))
U41_gga(X1, X2, X3, appcH_out_gga(X2, X3, X4)) → appcH_out_gga(cons(X1, X2), X3, cons(X1, X4))
appcG_in_aag(cons(a, cons(b, X1))) → appcG_out_aag(nil, X1, cons(a, cons(b, X1)))
appcG_in_aag(cons(X1, X4)) → U40_aag(X1, X4, appcG_in_aag(X4))
U40_aag(X1, X4, appcG_out_aag(X2, X3, X4)) → appcG_out_aag(cons(X1, X2), X3, cons(X1, X4))
appcF_in_gggga(nil, X1, X2, X3) → appcF_out_gggga(nil, X1, X2, X3, cons(s(a, s(X1, X2), b), X3))
appcF_in_gggga(cons(X1, X2), X3, X4, X5) → U39_gggga(X1, X2, X3, X4, X5, appcF_in_gggga(X2, X3, X4, X5))
U39_gggga(X1, X2, X3, X4, X5, appcF_out_gggga(X2, X3, X4, X5, X6)) → appcF_out_gggga(cons(X1, X2), X3, X4, X5, cons(X1, X6))
appcE_in_aaaag(cons(a, cons(s(X1, X2), cons(b, X3)))) → appcE_out_aaaag(nil, X1, X2, X3, cons(a, cons(s(X1, X2), cons(b, X3))))
appcE_in_aaaag(cons(X1, X6)) → U38_aaaag(X1, X6, appcE_in_aaaag(X6))
U38_aaaag(X1, X6, appcE_out_aaaag(X2, X3, X4, X5, X6)) → appcE_out_aaaag(cons(X1, X2), X3, X4, X5, cons(X1, X6))
appcC_in_aaaaag(cons(a, cons(s(X1, X2, X3), cons(b, X4)))) → appcC_out_aaaaag(nil, X1, X2, X3, X4, cons(a, cons(s(X1, X2, X3), cons(b, X4))))
appcC_in_aaaaag(cons(X1, X7)) → U36_aaaaag(X1, X7, appcC_in_aaaaag(X7))
U36_aaaaag(X1, X7, appcC_out_aaaaag(X2, X3, X4, X5, X6, X7)) → appcC_out_aaaaag(cons(X1, X2), X3, X4, X5, X6, cons(X1, X7))

The set Q consists of the following terms:

appcC_in_aaaaag(x0)
U36_aaaaag(x0, x1, x2)
appcI_in_ggggga(x0, x1, x2, x3, x4)
U37_ggggga(x0, x1, x2, x3, x4, x5, x6)
U42_gggggga(x0, x1, x2, x3, x4, x5, x6)
appcE_in_aaaag(x0)
U38_aaaag(x0, x1, x2)
appcF_in_gggga(x0, x1, x2, x3)
U39_gggga(x0, x1, x2, x3, x4, x5)
appcG_in_aag(x0)
U40_aag(x0, x1, x2)
appcH_in_gga(x0, x1)
U41_gga(x0, x1, x2, x3)

We have to consider all (P,Q,R)-chains.

(68) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 4 less nodes.

(69) Obligation:

Q DP problem:
The TRS P consists of the following rules:

PARSEA_IN_GA(X1) → U20_GA(X1, appcG_in_aag(X1))
U20_GA(X1, appcG_out_aag(X3, X4, X1)) → U22_GA(X1, appcH_in_gga(X3, X4))
U22_GA(X1, appcH_out_gga(X3, X4, X5)) → PARSEA_IN_GA(X5)

The TRS R consists of the following rules:

appcI_in_ggggga(nil, X1, X2, X3, X4) → appcI_out_ggggga(nil, X1, X2, X3, X4, cons(s(a, s(X1, X2, X3), b), X4))
appcI_in_ggggga(cons(X1, X2), X3, X4, X5, X6) → U37_ggggga(X1, X2, X3, X4, X5, X6, appcI_in_ggggga(X2, X3, X4, X5, X6))
U42_gggggga(X1, X2, X3, X4, X5, X6, appcI_out_ggggga(X2, X3, X4, X5, X6, X7)) → appcD_out_gggggga(X1, X2, X3, X4, X5, X6, cons(X1, X7))
U37_ggggga(X1, X2, X3, X4, X5, X6, appcI_out_ggggga(X2, X3, X4, X5, X6, X7)) → appcI_out_ggggga(cons(X1, X2), X3, X4, X5, X6, cons(X1, X7))
appcH_in_gga(nil, X1) → appcH_out_gga(nil, X1, cons(s(a, b), X1))
appcH_in_gga(cons(X1, X2), X3) → U41_gga(X1, X2, X3, appcH_in_gga(X2, X3))
U41_gga(X1, X2, X3, appcH_out_gga(X2, X3, X4)) → appcH_out_gga(cons(X1, X2), X3, cons(X1, X4))
appcG_in_aag(cons(a, cons(b, X1))) → appcG_out_aag(nil, X1, cons(a, cons(b, X1)))
appcG_in_aag(cons(X1, X4)) → U40_aag(X1, X4, appcG_in_aag(X4))
U40_aag(X1, X4, appcG_out_aag(X2, X3, X4)) → appcG_out_aag(cons(X1, X2), X3, cons(X1, X4))
appcF_in_gggga(nil, X1, X2, X3) → appcF_out_gggga(nil, X1, X2, X3, cons(s(a, s(X1, X2), b), X3))
appcF_in_gggga(cons(X1, X2), X3, X4, X5) → U39_gggga(X1, X2, X3, X4, X5, appcF_in_gggga(X2, X3, X4, X5))
U39_gggga(X1, X2, X3, X4, X5, appcF_out_gggga(X2, X3, X4, X5, X6)) → appcF_out_gggga(cons(X1, X2), X3, X4, X5, cons(X1, X6))
appcE_in_aaaag(cons(a, cons(s(X1, X2), cons(b, X3)))) → appcE_out_aaaag(nil, X1, X2, X3, cons(a, cons(s(X1, X2), cons(b, X3))))
appcE_in_aaaag(cons(X1, X6)) → U38_aaaag(X1, X6, appcE_in_aaaag(X6))
U38_aaaag(X1, X6, appcE_out_aaaag(X2, X3, X4, X5, X6)) → appcE_out_aaaag(cons(X1, X2), X3, X4, X5, cons(X1, X6))
appcC_in_aaaaag(cons(a, cons(s(X1, X2, X3), cons(b, X4)))) → appcC_out_aaaaag(nil, X1, X2, X3, X4, cons(a, cons(s(X1, X2, X3), cons(b, X4))))
appcC_in_aaaaag(cons(X1, X7)) → U36_aaaaag(X1, X7, appcC_in_aaaaag(X7))
U36_aaaaag(X1, X7, appcC_out_aaaaag(X2, X3, X4, X5, X6, X7)) → appcC_out_aaaaag(cons(X1, X2), X3, X4, X5, X6, cons(X1, X7))

The set Q consists of the following terms:

appcC_in_aaaaag(x0)
U36_aaaaag(x0, x1, x2)
appcI_in_ggggga(x0, x1, x2, x3, x4)
U37_ggggga(x0, x1, x2, x3, x4, x5, x6)
U42_gggggga(x0, x1, x2, x3, x4, x5, x6)
appcE_in_aaaag(x0)
U38_aaaag(x0, x1, x2)
appcF_in_gggga(x0, x1, x2, x3)
U39_gggga(x0, x1, x2, x3, x4, x5)
appcG_in_aag(x0)
U40_aag(x0, x1, x2)
appcH_in_gga(x0, x1)
U41_gga(x0, x1, x2, x3)

We have to consider all (P,Q,R)-chains.

(70) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(71) Obligation:

Q DP problem:
The TRS P consists of the following rules:

PARSEA_IN_GA(X1) → U20_GA(X1, appcG_in_aag(X1))
U20_GA(X1, appcG_out_aag(X3, X4, X1)) → U22_GA(X1, appcH_in_gga(X3, X4))
U22_GA(X1, appcH_out_gga(X3, X4, X5)) → PARSEA_IN_GA(X5)

The TRS R consists of the following rules:

appcH_in_gga(nil, X1) → appcH_out_gga(nil, X1, cons(s(a, b), X1))
appcH_in_gga(cons(X1, X2), X3) → U41_gga(X1, X2, X3, appcH_in_gga(X2, X3))
U41_gga(X1, X2, X3, appcH_out_gga(X2, X3, X4)) → appcH_out_gga(cons(X1, X2), X3, cons(X1, X4))
appcG_in_aag(cons(a, cons(b, X1))) → appcG_out_aag(nil, X1, cons(a, cons(b, X1)))
appcG_in_aag(cons(X1, X4)) → U40_aag(X1, X4, appcG_in_aag(X4))
U40_aag(X1, X4, appcG_out_aag(X2, X3, X4)) → appcG_out_aag(cons(X1, X2), X3, cons(X1, X4))

The set Q consists of the following terms:

appcC_in_aaaaag(x0)
U36_aaaaag(x0, x1, x2)
appcI_in_ggggga(x0, x1, x2, x3, x4)
U37_ggggga(x0, x1, x2, x3, x4, x5, x6)
U42_gggggga(x0, x1, x2, x3, x4, x5, x6)
appcE_in_aaaag(x0)
U38_aaaag(x0, x1, x2)
appcF_in_gggga(x0, x1, x2, x3)
U39_gggga(x0, x1, x2, x3, x4, x5)
appcG_in_aag(x0)
U40_aag(x0, x1, x2)
appcH_in_gga(x0, x1)
U41_gga(x0, x1, x2, x3)

We have to consider all (P,Q,R)-chains.

(72) QReductionProof (EQUIVALENT transformation)

We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

appcC_in_aaaaag(x0)
U36_aaaaag(x0, x1, x2)
appcI_in_ggggga(x0, x1, x2, x3, x4)
U37_ggggga(x0, x1, x2, x3, x4, x5, x6)
U42_gggggga(x0, x1, x2, x3, x4, x5, x6)
appcE_in_aaaag(x0)
U38_aaaag(x0, x1, x2)
appcF_in_gggga(x0, x1, x2, x3)
U39_gggga(x0, x1, x2, x3, x4, x5)

(73) Obligation:

Q DP problem:
The TRS P consists of the following rules:

PARSEA_IN_GA(X1) → U20_GA(X1, appcG_in_aag(X1))
U20_GA(X1, appcG_out_aag(X3, X4, X1)) → U22_GA(X1, appcH_in_gga(X3, X4))
U22_GA(X1, appcH_out_gga(X3, X4, X5)) → PARSEA_IN_GA(X5)

The TRS R consists of the following rules:

appcH_in_gga(nil, X1) → appcH_out_gga(nil, X1, cons(s(a, b), X1))
appcH_in_gga(cons(X1, X2), X3) → U41_gga(X1, X2, X3, appcH_in_gga(X2, X3))
U41_gga(X1, X2, X3, appcH_out_gga(X2, X3, X4)) → appcH_out_gga(cons(X1, X2), X3, cons(X1, X4))
appcG_in_aag(cons(a, cons(b, X1))) → appcG_out_aag(nil, X1, cons(a, cons(b, X1)))
appcG_in_aag(cons(X1, X4)) → U40_aag(X1, X4, appcG_in_aag(X4))
U40_aag(X1, X4, appcG_out_aag(X2, X3, X4)) → appcG_out_aag(cons(X1, X2), X3, cons(X1, X4))

The set Q consists of the following terms:

appcG_in_aag(x0)
U40_aag(x0, x1, x2)
appcH_in_gga(x0, x1)
U41_gga(x0, x1, x2, x3)

We have to consider all (P,Q,R)-chains.

(74) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04,JAR06].


The following pairs can be oriented strictly and are deleted.


U20_GA(X1, appcG_out_aag(X3, X4, X1)) → U22_GA(X1, appcH_in_gga(X3, X4))
The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial interpretation [POLO]:

POL(PARSEA_IN_GA(x1)) = 1 + x1   
POL(U20_GA(x1, x2)) = 1 + x2   
POL(U22_GA(x1, x2)) = x2   
POL(U40_aag(x1, x2, x3)) = x1 + x3   
POL(U41_gga(x1, x2, x3, x4)) = x1 + x4   
POL(a) = 0   
POL(appcG_in_aag(x1)) = x1   
POL(appcG_out_aag(x1, x2, x3)) = x1 + x2   
POL(appcH_in_gga(x1, x2)) = x1 + x2   
POL(appcH_out_gga(x1, x2, x3)) = 1 + x3   
POL(b) = 1   
POL(cons(x1, x2)) = x1 + x2   
POL(nil) = 1   
POL(s(x1, x2)) = 0   

The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:

appcG_in_aag(cons(a, cons(b, X1))) → appcG_out_aag(nil, X1, cons(a, cons(b, X1)))
appcG_in_aag(cons(X1, X4)) → U40_aag(X1, X4, appcG_in_aag(X4))
appcH_in_gga(nil, X1) → appcH_out_gga(nil, X1, cons(s(a, b), X1))
appcH_in_gga(cons(X1, X2), X3) → U41_gga(X1, X2, X3, appcH_in_gga(X2, X3))
U41_gga(X1, X2, X3, appcH_out_gga(X2, X3, X4)) → appcH_out_gga(cons(X1, X2), X3, cons(X1, X4))
U40_aag(X1, X4, appcG_out_aag(X2, X3, X4)) → appcG_out_aag(cons(X1, X2), X3, cons(X1, X4))

(75) Obligation:

Q DP problem:
The TRS P consists of the following rules:

PARSEA_IN_GA(X1) → U20_GA(X1, appcG_in_aag(X1))
U22_GA(X1, appcH_out_gga(X3, X4, X5)) → PARSEA_IN_GA(X5)

The TRS R consists of the following rules:

appcH_in_gga(nil, X1) → appcH_out_gga(nil, X1, cons(s(a, b), X1))
appcH_in_gga(cons(X1, X2), X3) → U41_gga(X1, X2, X3, appcH_in_gga(X2, X3))
U41_gga(X1, X2, X3, appcH_out_gga(X2, X3, X4)) → appcH_out_gga(cons(X1, X2), X3, cons(X1, X4))
appcG_in_aag(cons(a, cons(b, X1))) → appcG_out_aag(nil, X1, cons(a, cons(b, X1)))
appcG_in_aag(cons(X1, X4)) → U40_aag(X1, X4, appcG_in_aag(X4))
U40_aag(X1, X4, appcG_out_aag(X2, X3, X4)) → appcG_out_aag(cons(X1, X2), X3, cons(X1, X4))

The set Q consists of the following terms:

appcG_in_aag(x0)
U40_aag(x0, x1, x2)
appcH_in_gga(x0, x1)
U41_gga(x0, x1, x2, x3)

We have to consider all (P,Q,R)-chains.

(76) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 2 less nodes.

(77) TRUE